coq - 寻找一些比赛技巧或车队模式

Question

我正在阅读 Computational Type Theory and Interactive Theorem Proving with Coq 这本书，并且 其中一个练习是让我写下类型的术语:

forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x

我尝试了显而易见的:

Fail Definition L7 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x :=
    fun (p:bool -> Prop) =>
        fun (x:bool) =>
            fun (tt:x = true -> p true) =>
                fun (ff:x = false -> p false) =>
                    match x with
                    | true  => tt (eq_refl true)
                    | false => ff (eq_refl false)
                    end.

和不太明显的:

Definition bool_dec : forall (x:bool), x = true \/ x = false :=
    fun (x:bool) =>
        match x with
        | true  => or_introl (eq_refl true)
        | false => or_intror (eq_refl false)
        end.

Fail Definition L8 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x :=
    fun (p:bool -> Prop) =>
        fun (x:bool) =>
            fun (tt:x = true -> p true) =>
                fun (ff:x = false -> p false) =>
                    match bool_dec x with
                    | or_introl p  => tt p
                    | or_intror p  => ff p
                    end.

我知道会有一个技巧 match ... in ... return ... 或一些护航模式业务，导致我陷入困境，但我一直花一个小时在这上面，想继续前进。谁能把我从痛苦中解救出来？

Answer 1

首先，您可以像这样在嵌套函数中使用一次关键字fun

fun (p:bool -> Prop)
    (x:bool)
    (tt:x = true -> p true)
    (ff:x = false -> p false) =>
      match x with
      | true  => tt (eq_refl true)
      | false => ff (eq_refl false)
      end.

现在，一个好的方法是使用策略生成证明(此类对象)，然后使用Print 来查看对象是什么。

Theorem L7 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x.
Proof.
  intros. destruct x.
  - apply H. reflexivity.
  - apply H0. reflexivity.
Qed.
Print L7.

输出将是

L7 = 
fun (p : bool -> Prop)
  (x : bool)
  (H : x = true -> p true)
  (H0 : x = false -> p false)
=>
(if x as b
  return
    ((b = true -> p true) ->
     (b = false -> p false) ->
     p b)
 then
  fun
    (H1 : true = true -> p true)
    (_ : true = false ->
         p false) => 
  H1 eq_refl
 else
  fun
    (_ : false = true -> p true)
    (H2 : false = false ->
          p false) =>
  H2 eq_refl) H H0
     : forall
         (p : bool -> Prop)
         (x : bool),
       (x = true -> p true) ->
       (x = false -> p false) ->
       p x

Arguments L7 _%function_scope
  _%bool_scope (_
  _)%function_scope