Commit df17e4c2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`iSimpl` tactic that `simpl`s the proofmode goal.

parent 0d6031e4
...@@ -413,6 +413,11 @@ Proof. ...@@ -413,6 +413,11 @@ Proof.
Qed. Qed.
(** * Basic rules *) (** * Basic rules *)
Lemma tac_eval Δ Q Q' :
Q = Q'
envs_entails Δ Q' envs_entails Δ Q.
Proof. by intros ->. Qed.
Lemma tac_assumption Δ i p P Q : Lemma tac_assumption Δ i p P Q :
envs_lookup i Δ = Some (p,P) FromAssumption p P Q envs_lookup i Δ = Some (p,P) FromAssumption p P Q
envs_entails Δ Q. envs_entails Δ Q.
......
...@@ -80,6 +80,13 @@ Ltac iStartProof := ...@@ -80,6 +80,13 @@ Ltac iStartProof :=
|apply tac_adequate] |apply tac_adequate]
end. end.
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
try iStartProof;
try (eapply tac_eval; [t; reflexivity|]).
Tactic Notation "iSimpl" := iEval simpl.
(** * Context manipulation *) (** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) := Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *) eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment