Skip to content

Commit

Permalink
fresher
Browse files Browse the repository at this point in the history
  • Loading branch information
@h0nzZik
h0nzZik committed Mar 19, 2024
1 parent 28f5e33 commit 056a086
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 31 deletions.
15 changes: 12 additions & 3 deletions minuska/theories/minusl_compile.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,7 @@ Definition compile' {Σ : StaticModel} {Act : Set}
(topSymbol cseqSymbol holeSymbol : symbol)
(continuationVariable : variable)
(isValue : Expression -> (list SideCondition))
(avoid : gset variable)
(d : MinusL_Decl Act)
: (list (RewritingRule Act))
:=
Expand All @@ -169,8 +170,9 @@ Definition compile' {Σ : StaticModel} {Act : Set}
| mld_context _ c h Hh scs Hhscs =>
let vars := vars_of_to_l2r c in
let scs_vars := elements (vars_of scs) in
let contVariable := fresh (h::(vars++scs_vars)) in
let dataVariable := fresh (h::contVariable::(vars++scs_vars)) in
let lavoid := elements avoid in
let contVariable := fresh (h::(vars++scs_vars++lavoid)) in
let dataVariable := fresh (h::contVariable::(vars++scs_vars++lavoid)) in
[
(ctx_heat
invisible_act
Expand All @@ -197,6 +199,13 @@ Definition compile {Σ : StaticModel}
(continuationVariable : variable)
: CompileT :=
fun D => concat (map (
compile' invisible_act topSymbol cseqSymbol holeSymbol continuationVariable (MinusL_isValue Act D)
compile'
invisible_act
topSymbol
cseqSymbol
holeSymbol
continuationVariable
(MinusL_isValue Act D)
(vars_of (mlld_isValue_scs Act D))
) (mlld_decls Act D))
.
58 changes: 30 additions & 28 deletions minuska/theories/minusl_compile_properties.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8423,8 +8423,8 @@ Proof.

assert (Hheat:
ctx_heat invisible_act topSymbol cseqSymbol holeSymbol
(fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs))))
(fresh (h:: (fresh (h :: (vars_of_to_l2r c ++ ( elements (vars_of scs))))) :: (vars_of_to_l2r c ++ elements (vars_of scs))))
(fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))))
(fresh (h:: (fresh (h :: (vars_of_to_l2r c ++ ( elements (vars_of scs) ++ (elements (vars_of iV_scs)))))) :: (vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))))
(MinusL_isValue Act (@mkMinusL_LangDef Σ Act iV_scs iV_var ds)) c h scs ∈ Γ).
{
rewrite elem_of_list_lookup in H.
Expand All @@ -8451,8 +8451,8 @@ Proof.

assert (Hcool:
ctx_cool invisible_act topSymbol cseqSymbol holeSymbol
(fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs))))
(fresh (h:: (fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs)))) :: (vars_of_to_l2r c ++ elements (vars_of scs))))
(fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))))
(fresh (h:: (fresh (h::(vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))))) :: (vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))))
(MinusL_isValue Act (@mkMinusL_LangDef Σ Act iV_scs iV_var ds)) c h ∈ Γ).
{
rewrite elem_of_list_lookup in H.
Expand Down Expand Up @@ -8549,8 +8549,8 @@ Proof.
}
}

remember (fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs))) as V1.
remember (fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))) as V2.
remember (fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))) as V1.
remember (fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))) as V2.

eapply frto_step with (t2 := (t_term topSymbol [(t_term cseqSymbol [r; (t_term cseqSymbol [ceval; cont])]); state1])).
{ apply Hheat. }
Expand Down Expand Up @@ -8608,7 +8608,7 @@ Proof.
(* V1 <> x *)
clear -Hx HeqV1.
intros HContra. subst.
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite <- vars_of_uglify in Hx.
ltac1:(set_solver).
Expand All @@ -8620,7 +8620,7 @@ Proof.
(* V2 <> x *)
clear -Hx HeqV2.
intros HContra. subst.
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite <- vars_of_uglify in Hx.
ltac1:(set_solver).
Expand All @@ -8640,7 +8640,7 @@ Proof.
{
clear -HeqV2.
intros HContra. subst.
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite <- HContra at 2.
ltac1:(set_solver).
Expand All @@ -8651,7 +8651,7 @@ Proof.
{
clear -HeqV1.
intros HContra. subst.
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HContra at 2.
ltac1:(set_solver).
Expand All @@ -8673,7 +8673,7 @@ Proof.
{
clear -HeqV2.
intros HContra. subst.
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HContra at 2.
ltac1:(set_solver).
Expand Down Expand Up @@ -8756,7 +8756,7 @@ Proof.
rewrite <- vars_of_uglify in Htmp.
clear -Htmp HeqV2.
subst V2.
assert (Htmp2: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp2: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -8774,7 +8774,7 @@ Proof.
rewrite <- vars_of_uglify in Htmp.
clear -Htmp HeqV1.
subst V1.
assert (Htmp2: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp2: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -8795,7 +8795,7 @@ Proof.
clear -HeqV2.
intros HContra.
subst.
assert (H': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (H': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite <- HContra at 2.
clear. ltac1:(set_solver).
Expand All @@ -8807,7 +8807,7 @@ Proof.
clear -HeqV1.
intros HContra.
subst.
assert (H': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (H': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HContra at 2.
clear. ltac1:(set_solver).
Expand All @@ -8825,7 +8825,7 @@ Proof.
subst h.
ltac1:(exfalso).
clear -HeqV2.
assert (Htmp: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV2 at 2.
ltac1:(set_solver).
Expand All @@ -8849,7 +8849,7 @@ Proof.
{
clear -Hx HeqV1.
intros HContra. subst.
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -8859,7 +8859,7 @@ Proof.
{
clear -Hx HeqV2.
intros HContra. subst.
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert(Hx': fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand Down Expand Up @@ -8943,7 +8943,7 @@ Proof.
rewrite <- vars_of_uglify in Htmp.
clear -Htmp HeqV2.
subst V2.
assert (Htmp2: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp2: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -8961,7 +8961,7 @@ Proof.
rewrite <- vars_of_uglify in Htmp.
clear -Htmp HeqV1.
subst V1.
assert (Htmp2: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp2: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -8978,7 +8978,7 @@ Proof.
ltac1:(exfalso).
subst h.
clear -HeqV1.
assert (Htmp1: fresh (V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV1 at 2.
ltac1:(set_solver).
Expand All @@ -8993,7 +8993,7 @@ Proof.
ltac1:(exfalso).
clear - HeqV2 Heq.
subst V1.
assert (Htmp1: fresh (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV2 at 2.
ltac1:(set_solver).
Expand All @@ -9013,7 +9013,7 @@ Proof.
ltac1:(exfalso).
subst h.
clear - HeqV2.
assert (Htmp1: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV2 at 2. ltac1:(set_solver).
}
Expand Down Expand Up @@ -9070,7 +9070,7 @@ Proof.
subst x.
rewrite <- vars_of_uglify in Hx.
clear - HeqV2 Hx.
assert (Htmp1: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -9084,7 +9084,7 @@ Proof.
subst x.
rewrite <- vars_of_uglify in Hx.
clear - HeqV1 Hx.
assert (Htmp1: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
ltac1:(set_solver).
}
Expand All @@ -9101,7 +9101,7 @@ Proof.
{
intros HContra. subst h.
clear - HeqV1.
assert (Htmp1: fresh (V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV1 at 2. ltac1:(set_solver).
}
Expand All @@ -9115,7 +9115,7 @@ Proof.
ltac1:(exfalso).
clear - HeqV2 Heq.
subst V1.
assert (Htmp1: fresh (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (h :: V2 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV2 at 2.
ltac1:(set_solver).
Expand All @@ -9133,7 +9133,7 @@ Proof.
{
intros HContra. subst h.
clear - HeqV2.
assert (Htmp1: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs)) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs))).
assert (Htmp1: fresh (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs))) ∈ (V2 :: V1 :: vars_of_to_l2r c ++ elements (vars_of scs) ++ (elements (vars_of iV_scs)))).
{
rewrite HeqV2 at 2. ltac1:(set_solver).
}
Expand Down Expand Up @@ -9170,9 +9170,11 @@ Proof.
{ apply H4. }
{
intros x Hx.
unfold Valuation in *.
destruct (decide (x = V2)).
{
subst x.
ltac1:(exfalso).
admit.
}
admit.
Expand Down

0 comments on commit 056a086

Please sign in to comment.