Commit 5a80357c authored by Michael Sammler's avatar Michael Sammler
Browse files

fix evar instantiation

parent 8d836361
Pipeline #41501 passed with stage
in 30 minutes and 46 seconds
......@@ -297,6 +297,12 @@ Ltac liUnfoldLetsInContext :=
end.
(** * Management of evars *)
Ltac liUnfoldAllEvars :=
repeat rewrite protected_eq;
repeat match goal with
| He := EVAR_ID _ |- _ => unfold He, EVAR_ID; clear He
end.
Ltac create_protected_evar A :=
(* necessary, otherwise pattern might not find all occurences later, see also instantiate protected *)
let A := eval cbn in A in
......@@ -304,7 +310,10 @@ Ltac create_protected_evar A :=
(* see https://stackoverflow.com/a/46178884*)
let c :=
match goal with
| _ => let x := fresh "x" in evar (x : A); pose (Hevar := EVAR_ID x : A); unfold x in Hevar; clear x
| _ =>
let x := fresh "x" in
unshelve evar (x : A); [ liUnfoldAllEvars; liUnfoldLetsInContext; shelve |];
pose (Hevar := EVAR_ID x : A); unfold x in Hevar; clear x
end in
Hevar.
......@@ -313,6 +322,9 @@ Ltac unfold_instantiated_evar_hook H := idtac.
Ltac unfold_instantiated_evar H :=
unfold_instantiated_evar_hook H;
(* first we need to rewrap unfolded evars in H*)
repeat match goal with
| He := EVAR_ID ?x2 |- _ => progress unfold He in H
end;
revert H;
repeat lazymatch goal with
| |- let _ := EVAR_ID ?body in _ =>
......@@ -332,6 +344,7 @@ Ltac unfold_instantiated_evar H :=
end
end
end;
(* This is copied from the end of instantiate_protected *)
let tmp := fresh "tmp" in
intros tmp;
pattern (protected tmp);
......@@ -364,19 +377,16 @@ Ltac instantiate_protected H' tac_with :=
cbn in (type of Hevar)
end
end;
(* This is copied from the end of unfold_instantiated_evar *)
let tmp := fresh "tmp" in
intros tmp;
unfold_instantiated_evar tmp
pattern (protected tmp);
simple refine (tac_protected_eq_app _ _ _);
unfold tmp, EVAR_ID; clear tmp
end.
Tactic Notation "liInst" hyp(H) open_constr(c) :=
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=c) in (Value of H)).
Ltac liUnfoldAllEvars :=
repeat rewrite protected_eq;
repeat match goal with
| He := EVAR_ID _ |- _ => unfold He, EVAR_ID; clear He
end.
Ltac unfold_instantiated_evars :=
repeat match goal with
| H := EVAR_ID ?x |- _ => assert_fails (is_evar x); unfold_instantiated_evar H
......@@ -388,8 +398,8 @@ Ltac solve_protected_eq :=
try (
liUnfoldAllEvars;
lazymatch goal with |- ?a = ?b => unify a b with typeclass_instances end;
(* For some weird reason we need to do this twice that the has_evar check works *)
lazymatch goal with |- ?a = ?b => unify a b with typeclass_instances end;
(* We need to solve the constraints for the has_evar to work *)
solve_constraints;
lazymatch goal with
| |- ?g => assert_fails (has_evar g)
end);
......
......@@ -98,13 +98,19 @@ Ltac liRInstantiateEvars_hook := idtac.
Ltac liRInstantiateEvars :=
liRInstantiateEvars_hook;
lazymatch goal with
| |- (_ < protected ?H)%nat _ => liInst H (S (protected (EVAR_ID _)))
| |- (_ < protected ?H)%nat _ =>
(* We would like to use [liInst H (S (protected (EVAR_ID _)))],
but this causes a Error: No such section variable or assumption
at Qed. time. Maybe this is related to https://github.com/coq/coq/issues/9937 *)
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((S (protected (EVAR_ID _))))) in (Value of H))
(* This is very hard to figure out for unification because of the
dependent types in with refinement. Unificaiton likes to unfold the
definition of ty without this. This is the reason why do_instantiate
evars must come before do_side_cond *)
| |- protected ?H = ( _ @ ?ty)%I _ => liInst H ((protected (EVAR_ID _)) @ ty)%I
| |- protected ?H = ty_of_rty (frac_ptr ?β _)%I _ => liInst H (frac_ptr β (protected (EVAR_ID _)))%I
| |- protected ?H = ( _ @ ?ty)%I _ =>
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((protected (EVAR_ID _)) @ ty)%I) in (Value of H))
| |- protected ?H = ty_of_rty (frac_ptr ?β _)%I _ =>
instantiate_protected (protected H) ltac:(fun H => instantiate (1:=((frac_ptr β (protected (EVAR_ID _)))%I)) in (Value of H))
| |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{_} (protected ?H)) _) => liInst H ty
| |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{protected ?H} _) _) => liInst H β
end.
......
......@@ -400,7 +400,7 @@ Section ptr.
T l = p - simplify_goal (p ◁ᵥ l @ ptr) T.
Proof. iIntros "HT". iExists _. iFrame. by iIntros (->). Qed.
Global Instance simplify_ptr_goal_val_inst (p : loc) l:
SimplifyGoalVal p (l @ ptr)%I (Some 50%N) :=
SimplifyGoalVal p (l @ ptr)%I (Some 10%N) :=
λ T, i2p (simplify_ptr_goal_val p l T).
Lemma find_in_context_type_loc_own l T:
......
Supports Markdown
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