Présentation de nouvelles hypothèses dans les locaux

Question

Mes objectifs actuels suivent:

n' : nat 
    IHn' : forall m : nat, n' + n' = m + m -> n' = m 
    m' : nat 
    H1 : n' + n' = m' + m' 
    ============================ 
    S n' = S m' 

Maintenant, je veux apply H1 dans IHn' de telle sorte que l'hypothèse suivante est introduite:

n' = m' 

J'ai essayé ceci:

apply H1 with (m := m') in IHn'. 

Mais cela me donne cette erreur:

Error: No such bound variable m. 

C'est le programme reproductible avec ces objectifs:

Theorem my_theorem : forall n m, 
    n + n = m + m -> n = m. 
Proof. 
    intros n. induction n as [| n']. 
    - simpl. 
    intros m H. 
    symmetry in H. 
    destruct m as [| m']. 
    + reflexivity. 
    + rewrite -> plus_Sn_m in H. 
     inversion H. 
    - simpl. 
    rewrite <- plus_n_Sm. 
    intros m. 
    intros H. 
    destruct m as [| m']. 
    + simpl in H. 
     inversion H. 
    + rewrite -> plus_Sn_m in H. 
     rewrite <- plus_n_Sm in H. 
     inversion H. 
Abort. 

Answer 1

Le problème est que vous avez eu votre apply en arrière. Vous devez écrire apply IHn' with (m := m') in H1. Notez que dans ce cas, il est prudent d'omettre la clause with (m := m'), puisque Coq est assez intelligent pour comprendre cette information par lui-même.