Ищете какой-нибудь матч-трюк или конвой - PullRequest
Новая
       5

Ищете какой-нибудь матч-трюк или конвой

3 голосов
/ 27 марта 2020

Я слежу за книгой «Вычислительная теория типов и интерактивная теорема, доказывающая с помощью 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 ... или какой-то бизнес с конвоем, что приведет к скучному моменту с моей стороны, но у меня есть потратил час на это и хотел бы двигаться дальше. Кто-нибудь может избавить меня от моих страданий?

Ответы [ 2 ]

4 голосов
/ 27 марта 2020

Во-первых, вы можете использовать ключевое слово 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
1 голос
/ 29 марта 2020

Благодаря Камьяру выше, я смог получить простое решение: 

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).
...