Commit 9af0d884 authored by Ralf Jung's avatar Ralf Jung

make the way iMod solves side-conditions consistent with iInv

parent 28e01a7a
...@@ -41,6 +41,11 @@ performance and horrible error messages, so we wrap it in a [once]. *) ...@@ -41,6 +41,11 @@ performance and horrible error messages, so we wrap it in a [once]. *)
Ltac iSolveTC := Ltac iSolveTC :=
solve [once (typeclasses eauto)]. solve [once (typeclasses eauto)].
(** Tactic used for solving side-conditions arising from TC resolution in iMod
and iInv. *)
Ltac iSolveSideCondition :=
try (split_and?; solve [ fast_done | solve_ndisj ]).
(** * Misc *) (** * Misc *)
Ltac iMissingHyps Hs := Ltac iMissingHyps Hs :=
...@@ -1005,7 +1010,7 @@ Tactic Notation "iModCore" constr(H) := ...@@ -1005,7 +1010,7 @@ Tactic Notation "iModCore" constr(H) :=
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality " P "in" Q fail "iMod: cannot eliminate modality " P "in" Q
|try fast_done (* optional side-condition *) |iSolveSideCondition
|env_reflexivity|]. |env_reflexivity|].
(** * Basic destruct tactic *) (** * Basic destruct tactic *)
...@@ -1920,7 +1925,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H ...@@ -1920,7 +1925,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
[iSolveTC || [iSolveTC ||
let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant " I fail "iInv: cannot eliminate invariant " I
|try (split_and?; solve [ fast_done | solve_ndisj ]) |iSolveSideCondition
|let R := fresh in intros R; eexists; split; [env_reflexivity|]; |let R := fresh in intros R; eexists; split; [env_reflexivity|];
(* Now we are left proving [envs_entails Δ'' R]. *) (* Now we are left proving [envs_entails Δ'' R]. *)
iSpecializePat H pats; last ( iSpecializePat H pats; last (
......
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