Comment tirer les rhs sur une égalité dans coq

Question

Si je donne les résultats suivants:

H : some complicated expression = some other complicated expression 

et je veux saisir

u := some other complicated expression 

sans hardcoding dans ma preuve (à l'aide pose)

est-il un moyen propre à faire en Ltac?

Answer 1

Je suis sûr qu'il ya d'autres façons de ATTLC de le faire, dans mon cas, je préfère utiliser le langage modèle contextuel de ssreflect pour le faire. (Vous aurez besoin d'installer le plug-in ou utiliser Coq> = 8.7 qui comprend ssreflect):

(* ce_i = complicated expression i *) 
Lemma example T (ce_1 ce_2 : T) (H : ce_1 = ce_2) : False. 
set u := (X in _ = X) in H. 

but résultant:

T : Type 
    ce_1, ce_2 : T 
    u := ce_2 : T 
    H : ce_1 = u 
    ============================ 
    False 

vous pouvez généralement affiner le modèle de plus en plus jusqu'à ce que vous obtenez une match assez stable.

Notez que cela arrive à être le premier exemple de la section 8.3 « modèles contextuels » dans le manuel ssreflect.

Answer 2

Voici une autre version, qui utilise Ltac et sa capacité à motif match sur les types de termes:

Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" ident(H') := 
    match type of H with _ = ?rhs => set (u := rhs) in H' end. 

Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" "*" := 
    match type of H with _ = ?rhs => set (u := rhs) in * end. 

Nous pouvons créer plus de variantes ci-dessus (voir, par exemple here). Voici comment l'utiliser:

Lemma example {T} (ce1 ce2 ce3 : T) (H1 : ce1 = ce2) (H2 : ce2 = ce3) : ce1 = ce3. 
Proof. 
    assign rhs of H1 to u in *. 

état Preuve:

u := ce2 : T 
    H1 : ce1 = u 
    H2 : u = ce3 
    ============================ 
    ce1 = ce3 

Encore une fois:

Undo. 
    assign rhs of H1 to u in H1. 

état Preuve:

u := ce2 : T 
    H1 : ce1 = u 
    H2 : ce2 = ce3 
    ============================ 
    ce1 = ce3