Как доказать «~ (nat = False)», «~ (nat = bool)» и «~ (nat = True)» в coq

Question

Следующие два предложения легко доказать.

Theorem nat_eq_nat : nat = nat. 
Proof. 
    trivial. 
Qed. 

Theorem True_neq_False : ~(True = False). 
Proof. 
    unfold not. 
    intros. 
    symmetry in H. 
    rewrite H. 
    trivial. 
Qed. 

Но когда я попытался доказать, несколько иное предложение ~(nat = False), я обнаружил, что переписывание тактика не работает. Он сообщает

Error: Refiner was given an argument "fun x : Set => x" of type "Set -> Set" instead of "Set -> Prop".

Итак, я попытался написать лемм.

Lemma Type_eq_prod : forall (a : Type) (b : Type), a = b -> (a -> b). 
Proof. 
    intros. 
    rewrite <- H. 
    trivial. 
Qed. 

Theorem nat_neq_False : ~(nat = False). 
Proof. 
    unfold not. 
    intros. 
    apply (Type_eq_prod nat False) in H. 
    inversion H. 
    apply 0. (*no subgoals left*) 

Все работает нормально до сих пор. Но когда я попытался передать его, он сообщил

Error: Illegal application (Type Error): 
The term "Type_eq_prod" of type "forall a b : Type, a = b -> a -> b" 
cannot be applied to the terms 
"nat" : "Set" 
"False" : "Prop" 
"H" : "nat = False" 
"0" : "nat" 
The 3rd term has type "nat = False" which should be coercible to 
"nat = False". 

Следующие два предложения, которые заставляют меня застревать.

Theorem nat_neq_bool : ~(nat = bool). 
Proof. 
    unfold not. 
    intros. 
Abort. 

Theorem nat_neq_true : ~(nat = True). 
Proof. 
    unfold not. 
    intros. 
Abort. 

Мои вопросы:

1.Why the rewrite tactic doesn't work with proposition ~(nat = False). 
2.Why can't I Qed it when there is no subgoals. 
3.How to prove the aborted propositions above or is it possible to prove or prove the negates of them in coq. 

Answer 1

1. переписывания тактика не работает из-за того, как Coq обрабатывает свои вселенные, Prop, Set и Type. Существует понятие о подпункте, которое позволяет использовать Prop, как если бы он был Set или Type. Вот почему вам было позволено написать nat = False в первую очередь, так как равенство допускается только между вещами того же типа. Проблема в том, что для Coq False : Prop отличается от False : Set. not определяется с помощью False : Prop, что означает, что этот переписать приведет к несоответствию, что объясняет полученное сообщение об ошибке.

   Вот аналогичные подходы, которые будут работать. Обратите внимание на явное принуждение к Set.

   Lemma nat_neq_False_2 : (nat = False) -> (False : Set). 
   Proof. 
       intros H. 
       rewrite <- H. 
       apply 0. 
   Qed. 
   
   Lemma nat_neq_False_3 : ~(nat = False). 
   Proof. 
       intros H. 
       destruct (nat_neq_False_2 H). 
   Qed. 
   

2. Когда вы пишете доказательство, используя тактику, Coq по существу строит доказательство термина внутренне, но на самом деле не его проверки типов. В этом смысле это немного похоже на метапрограммирование. Как только вы нажмете Qed, термин, который был построен по тактике, отправляется в typechecker, чтобы убедиться, что все в порядке. В большинстве случаев тактика производит доказательства, которые являются правильными, но каждый раз время от времени обнаруживаются доказательства, которые не принимаются, и ваш пример является примером этого.

   Сообщение об ошибке, которое было напечатано, было не очень ясным, но можно лучше понять, что происходит с помощью команды Set Printing All, что заставляет Coq печатать все термины и инструкции без обозначений и показывать неявные аргументы. Это то, что ваше сообщение об ошибке будет, когда это делать:

   Set Printing All. 
   
   Lemma Type_eq_prod : forall (a : Type) (b : Type), a = b -> (a -> b). 
   Proof. 
       intros. 
       rewrite <- H. 
       trivial. 
   Qed. 
   
   Theorem nat_neq_False : ~(nat = False). 
   Proof. 
       unfold not. 
       intros. 
       apply (Type_eq_prod nat False) in H. 
       inversion H. 
       apply 0. (*no subgoals left*) 
   Qed. 
   
   
   (* Error: Illegal application (Type Error): *) 
   (* The term "Type_eq_prod" of type "forall a b : Type, @eq Type a b -> a -> b" *) 
   (* cannot be applied to the terms *) 
   (* "nat" : "Set" *) 
   (* "False" : "Prop" *) 
   (* "H" : "@eq Set nat False" *) 
   (* "O" : "nat" *) 
   (* The 3rd term has type "@eq Set nat False" which should be coercible to *) 
   (* "@eq Type nat False". *) 
   

   Там, мы можем видеть, что проблема заключается в том, что опять-таки несовпадение вселенной: один равенство в Type, в то время как другой находится в Set. Есть несколько способов исправить это; самый простой, вероятно, изменить свою первую теорему:

   Lemma Type_eq_prod : forall (a : Set) (b : Set), a = b -> (a -> b). 
   

3. Оба предложения доказуемы в Coq. В базовой теории Coq единственный способ показать, что простые типы, такие как и bool, различны по аргументам мощности.Таким образом, nat <> bool, потому что bool имеет только два элемента, тогда как nat имеет больше, чем это. Таким образом, показывая, что bool имеет два элемента, можно переписать равенство nat = bool, чтобы узнать, что nat также должен иметь два элемента, а затем использовать это, чтобы получить противоречие. Аналогичный аргумент показал бы, что nat <> True.