CODEWITHSUNDEEP
coqcoq-tactic
k_g
k_g

Reputation: 4464

How to pull the rhs out of an equality in coq

If I have the following:

H : some complicated expression = some other complicated expression

and I want to grab

u := some other complicated expression

without hardcoding it into my proof (i.e., using pose)

Is there a clean way to do this in LTac?

Upvotes: 3

Views: 125

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

Here is another version, which uses Ltac and its ability to pattern-match on types of terms:

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.

We can create more variants of the above (see e.g. here). Here is how to use it:

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

Proof state:

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

One more time:

  Undo.
  assign rhs of H1 to u in H1.

Proof state:

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

Upvotes: 3

ejgallego
ejgallego

Reputation: 6852

I am sure there are other ltac ways to do it, in my case I prefer to use SSReflect's contextual pattern language to do it. (You'll need to install the plugin or use Coq >= 8.7 which includes 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.

resulting goal:

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

Usually you can refine the pattern more and more until you get a pretty stable match.

Note that this happens to be the first example of the section 8.3 "Contextual patterns" in the SSReflect manual.

Upvotes: 3

Related Questions