LhsRhsTactic

Pierre Letouzey edited this page Oct 27, 2017 · 5 revisions

LHS & RHS

LHS means “left-hand side”. It returns the term on the left hand side of an equality or inequality.

Ltac LHS :=
match goal with
| |-(?a = _) => constr: a
| |-(_ ?a _) => constr: a
end.

For example you can use this to write a tactic that proves the cofixpoint equations of streams:

Ltac decomp_stream := intros; let L := LHS in rewrite (Streams.unfold_Stream L); reflexivity.

RHS means “right-hand side”. It returns the term on the right hand side of an equality or inequality.

Ltac RHS :=
match goal with
| |-(_ = ?a) => constr: a
| |-(_ _ ?a) => constr: a
end.

We can make special tactics for replace LHS and replace RHS that give similar functionality to step.

Tactic Notation "replace" "LHS" "with" constr (a) "by" tactic (t) :=
match goal with
| |-(?r ?b ?c) =>
  let Z := fresh "Z" in
  (change (let Z:=b in r Z c);intro Z;setoid_replace Z with a;
   [unfold Z; clear Z|unfold Z; clear Z; solve [ t ]])
end.
Tactic Notation "replace" "LHS" "with" constr (a) :=
match goal with
| |-(?r ?b ?c) =>
  let Z := fresh "Z" in
  (change (let Z:=b in r Z c);intro Z;setoid_replace Z with a;
   unfold Z; clear Z)
end.
Tactic Notation "replace" "RHS" "with" constr (a) "by" tactic (t) :=
match goal with
| |-(?r ?b ?c) =>
  let Z := fresh "Z" in
  (change (let Z:=c in r b Z);intro Z;setoid_replace Z with a;
   [unfold Z; clear Z|unfold Z; clear Z; solve [ t ]])
end.
Tactic Notation "replace" "RHS" "with" constr (a) :=
match goal with
| |-(?r ?b ?c) =>
  let Z := fresh "Z" in
  (change (let Z:=c in r b Z);intro Z;setoid_replace Z with a;
   unfold Z; clear Z)
end.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.