Commit c8780ac2 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

extend the closedness solver a bit

parent 5a3c7184
From stdpp Require Import base relations.
From iris Require Import prelude.
From semantics.systemf Require Export lang notation types bigstep.
From semantics.lib Require Import facts.
From semantics.systemf Require Export lang notation parallel_subst types bigstep.
Lemma list_subseteq_cons {X} (A B : list X) x : A B x :: A x :: B.
Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed.
Lemma list_subseteq_cons_binder A B x : A B x :b: A x :b: B.
Proof. destruct x; first done. apply list_subseteq_cons. Qed.
Ltac simplify_list_elem :=
simpl;
repeat match goal with
| |- ?x ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
| |- _ [] => apply not_elem_of_nil
| |- _ _ :: _ => apply not_elem_of_cons; split
end; try fast_done.
Ltac simplify_list_subseteq :=
simpl;
repeat match goal with
| |- ?x :: _ ?x :: _ => apply list_subseteq_cons_l
| |- ?x :: _ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
| |- elements _ elements _ => apply elements_subseteq; set_solver
| |- [] _ => apply list_subseteq_nil
| |- ?x :b: _ ?x :b: _ => apply list_subseteq_cons_binder
end;
try fast_done.
(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
Ltac closed_solver :=
simpl;
repeat match goal with
Ltac simplify_closed :=
simpl; intros;
repeat match goal with
| |- closed _ _ => unfold closed; simpl
| |- Is_true (is_closed [] _) => first [assumption | done]
| |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[closed_solver]
| |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
| |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
| |- Is_true (is_closed _ _) => eassumption
| |- Is_true (_ && true) => rewrite andb_true_r
| |- Is_true (true && _) => rewrite andb_true_l
| |- Is_true (?a && ?a) => rewrite andb_diag
| |- Is_true (_ && _) => simpl; rewrite !andb_True; split_and!
| |- [] _ => apply list_subseteq_nil
| |- ?x :: _ ?x :: _ => apply list_subseteq_cons
| |- ?x :b: _ ?x :b: _ => apply list_subseteq_cons_binder
| |- _ [] => apply not_elem_of_nil
| |- _ _ :: _ => apply not_elem_of_cons; split
| |- _ ?A => match type of A with | list _ => simplify_list_subseteq end
| |- _ ?A => match type of A with | list _ => simplify_list_elem end
| |- _ ?A => match type of A with | list _ => simplify_list_elem end
| |- _ _ => congruence
| H : closed _ _ |- _ => unfold closed in H; simpl in H
| H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
| H : _ _ |- _ => destruct H
| |- Is_true (bool_decide (_ _)) => apply bool_decide_pack; set_solver
end; try fast_done.
Ltac bs_step_det :=
repeat match goal with
| |- big_step ?e _ =>
......@@ -42,14 +68,14 @@ Ltac bs_step_det :=
| context[decide (_ _)] => rewrite decide_False; [ | congruence]
(* if we have a substitution that didn't simplify, try to show that it's closed *)
(* we don't make any attempt to solve it if it isn't closed under [] *)
| context[lang.subst _ _ ?e] => is_var e; rewrite subst_is_closed_nil; last solve[closed_solver]
| context[lang.subst _ _ (of_val ?v)] => is_var v; rewrite subst_is_closed_nil; last solve[closed_solver]
| context[lang.subst _ _ ?e] => is_var e; rewrite subst_is_closed_nil; last solve[simplify_closed]
| context[lang.subst _ _ (of_val ?v)] => is_var v; rewrite subst_is_closed_nil; last solve[simplify_closed]
(* try to use a [big_step] assumption, or else apply a constructor *)
| _ => first [eassumption | econstructor]
end
| |- bin_op_eval _ _ _ = _ =>
simpl; reflexivity
end; closed_solver.
end; simplify_closed.
Ltac bs_steps_det := repeat bs_step_det.
Ltac map_solver :=
......
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