égalité Decomposing des constructeurs coq

Question

Souvent en Coq je me retrouve à faire ce qui suit: Je l'objectif preuve, par exemple:

some_constructor a c d = some_constructor b c d 

Et je vraiment besoin de prouver a = b parce que tout le reste est identique de toute façon, Je fais:

assert (a = b). 

prouver ensuite que subgoal, puis

rewrite H. 
reflexivity. 

termine la preuve.

Mais il semble que ce soit juste un encombrement inutile pour avoir ceux qui traînent au fond de ma preuve. Y a-t-il une stratégie générale dans Coq pour prendre une égalité de constructeurs et la diviser en une égalité de paramètres constructeurs, un peu comme un split mais pour des égalités plutôt que des conjonctions.

Answer 1

En particulier, la norme Coq fournit la tactique f_equal.

Inductive u : Type := U : nat -> nat -> nat -> u. 

Lemma U1 x y z1 z2 : U x y z1 = U x y z2. 
f_equal 

En outre, ssreflect fournit une tactique congruence polyvalente congr.

Answer 2

Vous pouvez utiliser les fonctions de recherche de Coq:

Search (?X _ = ?X _). 
    Search (_ _ = _ _). 

Parmi bruit, il révèle un lemme

f_equal: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y 

Et ses frères et sœurs pour égalités plusieurs arguments: f_equal2 ... f_equal5 (en Coq version 8.4).

Voici un exemple:

Inductive silly : Set := 
    | some_constructor : nat -> nat -> nat -> silly 
    | another_constructor : nat -> nat -> silly. 

Goal forall x y, 
    x = 42 -> 
    y = 6 * 7 -> 
    some_constructor x 0 1 = some_constructor y 0 1. 
    intros x y Hx Hy. 
    apply f_equal3; try reflexivity. 

À ce stade, tout ce que vous devez prouver est x = y.