forall égalité en Coq

Je suis en train de prouver l'égalité suivante:forall égalité en Coq

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A) 
(ic0 : 0 < S n) (ic1 : 0 mod S n < S n): 
    gen (n - n) ic1 = gen 0 ic0.

Le n-n est 0 par Nat.sub_diag et 0 mod S n est également 0 par Nat.mod_0_l. Cependant, je ne pouvais pas facilement appliquer ces lemmes aux types. J'ai essayé astuce habituelle de remember/rewrite/subst mais subst pièce tombe en panne:

remember (gen (n-n)) as Q. 
    remember (n-n) as Q1. 
    rewrite Nat.sub_diag in HeqQ1. 
    subst.

post-scriptum Cette question peut utiliser un meilleur titre. Veuillez suggérer.

Source

2017-10-11 krokodil

Je pense que la bibliothèque Coq pourrait avoir une preuve d'unicité de 'lt nm' quelque part - et sinon, je pense que je l'ai vu flotter quelques fois sur coq-club alors vous pourriez essayer de chercher dans les archives de la liste de diffusion . Ensuite, vous pouvez généraliser 'ic0' et' ic1', ce qui devrait permettre la réécriture. –

ne sais pas comment utiliser l'unicité ici. En passant, je suis d'accord pour utiliser l'inadéquation de preuve, si cela aide ... – krokodil

La tactique subst échoue car remember est buggé; J'ai signalé ce bug here. (En guise de bonne santé, cocher, terminer un but avec abstract admit, où admit vient de Coq.Compat.AdmitAxiom, ne devrait jamais échouer avec une erreur de type.Si c'est le cas, cela signifie qu'il y a un bug dans Coq (ou un plugin que vous utilisez).)

Voici une preuve de travail (testé en 8.6.1 et 8.7 + beta2):

Require Import Coq.Arith.Arith. 

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A) 
     (ic0 : 0 < S n) (ic1 : 0 mod S n < S n): 
    gen (n - n) ic1 = gen 0 ic0. 
Proof. 
    revert ic0 ic1; simpl; rewrite Nat.sub_diag; intros ic0 ic1. 
    apply f_equal, le_unique. 
Qed.

Notez que vous avez la chance, dans un certain sens, que n - n et 0 mod S n sont judgmentally égaux. L'utilisation de simpl expose ce fait et permet à rewrite de fonctionner.

Source

2017-10-11 05:30:34

forall égalité en Coq

Répondre

Questions connexes