Looking for some match trick or convoy pattern

user_5339728 0
Viewed 56

I am following the book Computational Type Theory and Interactive Theorem Proving with Coq, and one of the exercises is for me to write of term of type:

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

I tried the obvious:

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.

and the less obvious:

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.

I know there is going to be a trick match ... in ... return ... or some convoy pattern business, leading to a duh moment on my part, but I have been spending an hour on this and would like to move on. Can anyone take me out of my misery?

coq
2 Answers

First, you can use keyword fun just once in nested function like this

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.

Now, a good way would be use tactics to generate a proof (an object of this type), then use Print to see what is the object.

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.

The output would be

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
user_57746610

Thanks to Kamyar above, I was able to obtain a simple solution:

Definition L8 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x :=
    fun (p:bool -> Prop) (x:bool) (H1:x = true -> p true) (H2:x = false -> p false) =>
        match x as b return x = b -> p b with
        | true  => H1
        | false => H2
        end (eq_refl x).
user_53397280
Related