Блог

Я новичок в coq и пытаюсь доказать эту теорему

 Inductive expression : Type :=
  | Var (n : nat)
.
.

Theorem variable_equality : forall x : nat, forall n : nat,
  ((equals x n) = true) -> (Var x = Var n).
 

Это определение equals

 
Fixpoint equals (n1 : nat) (n2 : nat) :=
  match (n1, n2) with
    | (O, O)      => true
    | (O, S n)    => false
    | (S n, O)    => false
    | (S n, S n') => equals n n'
  end.

 

Пока это мое решение

 Proof.
intros x n. induction x as [| x' IH].
  - destruct n. 
      reflexivity.
      simpl. intro. 
 

и в итоге я получаю что-то вроде этого

 1 subgoal 
n : nat
H : false = true
-------------------------
Var 0 = Var (S n)
 

Я понимаю, что этот вывод означает, что предложение «Var 0 = Var (S n)» должно следовать из предложения «false = true», если теорема должна быть правильной, но я не знаю, что с этим делать, и продвигаюсь вперед с моим доказательством.

Другой вариант, discriminate который является специальной тактикой для такого рода целей: предполагается, что он решает именно такие проблемы (т. Е. Равенства различных конструкторов в ваших гипотезах) и не более.

 Goal false = true -> False.
discriminate.
Qed.
 

Кроме того, это терминатор, что означает, что он терпит неудачу, если цель не решена после его использования, inversion в отличие от и congruence который будет успешным в некоторых случаях, когда они не решают ожидаемую проблему и преуспевают «неожиданным» образом.

например

 Goal true = true -> True.
inversion 1.
Qed.
 

и

 Goal true = true -> S 1 = S 1.
congruence.
Qed.
 

Лично я использую by [] (который также является терминатором) из ssreflect для такого рода целей и для всех «тривиальных» целей подобного рода:

 Require Import ssreflect.

Goal false = true -> False.
by [].
Qed.
 

Другой вариант: вместо inversion , используйте congruence :

 Goal false=true -> False.
  congruence.
Qed.
 

Эта тактика предназначена для использования несвязности конструкторов.

Используйте inversion такую гипотезу, как в:

 Goal false=true -> False.
intros H.
inversion H.
Qed.