Coq débutant - Prouver un lemme de base

Question

Je suis un débutant avec Coq alors peut-être ma question semble être une question stupide, mais voici mon problème:

I défini un module simple dans lequel je définissais un type T et une fonction « my_custom_equal »:

Definition T := nat. 

    Fixpoint my_custom_equal (x y : T) := 
    match x, y with 
     | O, O => true 
     | O, S _ => false 
     | S _, O => false 
     | S sub_x, S sub_y => my_custom_equal sub_x sub_y 
    end. 

    Lemma my_custom_reflex : forall x : T, my_custom_equal x x = true. 
    Proof. 
    intros. 
    induction x. 
    simpl. 
    reflexivity. 
    simpl. 
    rewrite IHx. 
    reflexivity. 
    Qed. 

    Lemma my_custom_unicite : forall x y : T, my_custom_equal x y = true -> x = y. 
    Proof. 
    intros. 
    induction x. 
    induction y. 
    reflexivity. 
    discriminate. 

    Qed. 

Comme vous pouvez le voir, il est pas vraiment compliqué, mais je reste coincé sur la preuve my_custom_unicite, j'arrive toujours au point où je dois prouver que « S x = y "et mon hypothèse sont seulement:

y : nat 
H : my_custom_equal 0 (S y) = true 
IHy : my_custom_equal 0 y = true -> 0 = y 
______________________________________(1/1) 
S x = y 

Je ne comprends pas comment réaliser cette preuve, pourriez-vous m'aider?

Merci!

Answer 1

Ceci est un piège typique pour les débutants. Le problème est que vous avez effectué l'induction sur x lorsque y a déjà été introduit dans votre contexte. À cause de cela, l'hypothèse d'induction que vous obtenez est pas assez générale: ce que vous voulez vraiment est d'avoir quelque chose comme

forall y, my_custom_equal x y = true -> x = y 

Notez que le forall supplémentaire. La solution est de mettre y de nouveau dans votre objectif:

Lemma my_custom_unicite : forall x y, my_custom_equal x y = true -> x = y. 
Proof. 
intros x y. revert y. 
induction x as [|x IH]. 
- intros []; easy. 
- intros [|y]; try easy. 
    simpl. 
    intros H. 
    rewrite (IH y H). 
    reflexivity. 
Qed. 

Essayez d'exécuter cette preuve interactive et comment vérifier l'hypothèse d'induction change lorsque vous atteignez le second cas.