Clever Geek Handbook

How to deduce rhs from equality in coq

If I have the following:

H : some complicated expression = some other complicated expression

and I want to capture

u := some other complicated expression

without hardcoding into my proof (i.e. using pose

)

Is there a clean way to do this in LTac?

+3


source to share


2 answers


I'm sure there are other ways to do this, but in my case I prefer to use the SSReflect context template language for this. (You 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.

target:



  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 fairly stable match.

Note that this is the first example of section 8.3 Context Templates in the SSReflect manual.

+3


source


Here's another version that uses Ltac and its ability to match patterns by term type:

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 variations above (see for example here ). Here's 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

Again:

  Undo.
  assign rhs of H1 to u in H1.

Proof state:



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


source






More articles:


All Articles