Skip to content

Clean up e-graph lemmas. #33

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
DIJamner wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Clean up e-graph lemmas. #33

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions src/Pyrosome/Tools/EGraph/AdapterGlue.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,7 +395,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb.
unfold vc in Hvc_rb.
specialize (Hvc_rb (snd (add_ctx succ sort_of l false false c (empty_egraph V_default X)))).
Expand Down Expand Up @@ -468,7 +468,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb2.
unfold vc in Hvc_rb2.
specialize (Hvc_rb2 e_open).
Expand Down Expand Up @@ -1437,7 +1437,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb2.
unfold vc in Hvc_rb2.
specialize (Hvc_rb2 e_open).
Expand Down Expand Up @@ -1989,7 +1989,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb.
unfold vc in Hvc_rb.
specialize (Hvc_rb e_open).
Expand Down Expand Up @@ -2118,7 +2118,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb.
unfold vc in Hvc_rb. specialize (Hvc_rb e_union). cbn [snd] in Hvc_rb.
specialize (Hvc_rb Hvc_union_ok).
Expand Down Expand Up @@ -2807,7 +2807,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb.
unfold vc in Hvc_rb.
specialize (Hvc_rb e_open).
Expand Down Expand Up @@ -2925,7 +2925,7 @@ Section WithVar.
V_trie V_trie_ok unit HX
(lang_model l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
(fun _ => True) rf)
rf)
as Hvc_rb.
unfold vc in Hvc_rb. specialize (Hvc_rb e_union). cbn [snd] in Hvc_rb.
specialize (Hvc_rb Hvc_union_ok).
Expand Down
30 changes: 15 additions & 15 deletions src/Pyrosome/Tools/EGraph/AddCtxInversion.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,11 +133,11 @@ Section WithVar.
pose proof (@rebuild_canon V V_Eqb V_Eqb_ok lt succ V_default
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X _ lang_model (lang_model_ok l Hsof Hwf)
fuel e1 ed_list Hok Hgwl) as [HdbT [Hmono _] ].
fuel ed_list e1 Hok Hgwl) as [HdbT [Hmono _] ].
eapply (@L_survive_canonical' V V_Eqb V_Eqb_ok lt succ V_default
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X _ lang_model (lang_model_ok l Hsof Hwf)
(S fuel) e1 a).
(S fuel) a e1).
+ exact Hok.
+ exact Hup.
+ exact HdbT.
Expand Down Expand Up @@ -272,7 +272,7 @@ Section WithVar.
pose proof (@rebuild_canon V V_Eqb V_Eqb_ok lt succ V_default
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X _ lang_model (lang_model_ok l Hsof Hwf)
fuel e1 ed_list Hok1 Hgwl) as (HdbT & Hmono & Hrev).
fuel ed_list e1 Hok1 Hgwl) as (HdbT & Hmono & Hrev).
(* --- canonicalizing survival --- *)
pose proof (rebuild_survives_canonical e1 (S fuel) Hok1 (ex_intro _ _ Hgwl) Hsucc) as Hsurv.
(* --- build Hsurv_exact from Hsurv (for use with atom_tree_sort_survives) --- *)
Expand Down Expand Up @@ -388,7 +388,7 @@ Section WithVar.
pose proof (@rebuild_canon V V_Eqb V_Eqb_ok lt succ V_default
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X _ lang_model (lang_model_ok l Hsof Hwf)
fuel e1 ed_list Hok1 Hgwl) as (HdbT & Hmono & Hrev).
fuel ed_list e1 Hok1 Hgwl) as (HdbT & Hmono & Hrev).
unfold ain, Semantics.atom_in_egraph in Hb. fold eF in Hb.
destruct (Hrev b Hb) as (a & Ha_e1_db & Hafn & Haargs).
assert (Ha_e1_in : ain a e1) by (unfold ain, Semantics.atom_in_egraph; exact Ha_e1_db).
Expand Down Expand Up @@ -606,7 +606,7 @@ Section WithVar.
pose proof (@alloc_opaque_rank_zero V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc.
pose proof (@alloc_opaque_egraph_ok V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_eg.
pose proof (@alloc_opaque_parents_keys_in_equiv V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_pke.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_ac.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX) as Halloc_ac.
unfold vc in Halloc, Halloc_eg, Halloc_pke, Halloc_ac.
specialize (Halloc e_sort). specialize (Halloc_eg e_sort). specialize (Halloc_pke e_sort). specialize (Halloc_ac e_sort).
destruct (alloc_opaque V succ V V_map V_map V_trie X e_sort) as [x' e_alloc] eqn:Heq_alloc.
Expand Down Expand Up @@ -940,7 +940,7 @@ Section WithVar.
pose proof (@alloc_opaque_rank_zero V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc.
pose proof (@alloc_opaque_egraph_ok V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_eg.
pose proof (@alloc_opaque_parents_keys_in_equiv V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_pke.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_ac.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX) as Halloc_ac.
unfold vc in Halloc, Halloc_eg, Halloc_pke, Halloc_ac.
specialize (Halloc e_sort). specialize (Halloc_eg e_sort). specialize (Halloc_pke e_sort). specialize (Halloc_ac e_sort).
destruct (alloc_opaque V succ V V_map V_map V_trie X e_sort) as [x' e_alloc] eqn:Heq_alloc.
Expand Down Expand Up @@ -1190,7 +1190,7 @@ Section WithVar.
pose proof (@alloc_opaque_rank_zero V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc.
pose proof (@alloc_opaque_egraph_ok V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_eg.
pose proof (@alloc_opaque_parents_keys_in_equiv V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_pke.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX lt_asymmetric lt_succ lt_trans) as Halloc_ac.
pose proof (@alloc_opaque_analyses_cover V V_Eqb V_Eqb_ok lt succ V V_map V_map V_map_ok V_trie X HX) as Halloc_ac.
unfold vc in Halloc, Halloc_eg, Halloc_pke, Halloc_ac.
specialize (Halloc e_inner). specialize (Halloc_eg e_inner). specialize (Halloc_pke e_inner). specialize (Halloc_ac e_inner).
destruct (alloc_opaque V succ V V_map V_map V_trie X e_inner) as [x' e_alloc] eqn:Heq_alloc.
Expand Down Expand Up @@ -2345,7 +2345,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Hafn_sof : atom_fn a = sort_of) by (rewrite Hafn; exact Hbfn).
pose proof (@Theorems.add_open_term'_keeps_sortof V V_Eqb V_Eqb_ok V_default V_map V_map_ok
Expand Down Expand Up @@ -2498,7 +2498,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Hafn_sof : atom_fn a = sort_of) by (rewrite Hafn; exact Hbfn).
pose proof (@Theorems.add_open_term'_keeps_sortof V V_Eqb V_Eqb_ok V_default V_map V_map_ok
Expand Down Expand Up @@ -2707,7 +2707,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Ha_eopen : @Semantics.atom_in_egraph V V V_map V_map V_trie X a e_open) by exact Ha_eopen_db.
assert (Hafn_ne : atom_fn a <> sort_of) by (rewrite Hafn; exact Hbfn).
Expand Down Expand Up @@ -2949,7 +2949,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Ha_eopen : @Semantics.atom_in_egraph V V V_map V_map V_trie X a e_open) by exact Ha_eopen_db.
assert (Hafn_ne : atom_fn a <> sort_of) by (rewrite Hafn; exact Hbfn).
Expand Down Expand Up @@ -4028,7 +4028,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Hafn_sof : atom_fn a = sort_of) by (rewrite Hafn; exact Hbfn).
pose proof (@Theorems.add_open_sort'_keeps_sortof V V_Eqb V_Eqb_ok V_default V_map V_map_ok
Expand Down Expand Up @@ -4190,7 +4190,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Ha_eopen : @Semantics.atom_in_egraph V V V_map V_map V_trie X a e_open) by exact Ha_eopen_db.
assert (Hafn_ne : atom_fn a <> sort_of) by (rewrite Hafn; exact Hbfn).
Expand Down Expand Up @@ -4494,7 +4494,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Hafn_sof : atom_fn a = sort_of) by (rewrite Hafn; exact Hbfn).
pose proof (@Theorems.add_open_sort'_keeps_sortof V V_Eqb V_Eqb_ok V_default V_map V_map_ok
Expand Down Expand Up @@ -4657,7 +4657,7 @@ Section WithVar.
V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok
X HX (Theorems.lang_model V sort_of l)
(@Theorems.lang_model_ok V V_Eqb V_Eqb_ok sort_of l Hsof Hwf)
fuel e_open ed_list Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
fuel ed_list e_open Hok_open Hgwl_open) as (HdbT & Hmono & Hrev).
destruct (Hrev b Hb) as (a & Ha_eopen_db & Hafn & Haargs).
assert (Ha_eopen : @Semantics.atom_in_egraph V V V_map V_map V_trie X a e_open) by exact Ha_eopen_db.
assert (Hafn_ne : atom_fn a <> sort_of) by (rewrite Hafn; exact Hbfn).
Expand Down
14 changes: 7 additions & 7 deletions src/Pyrosome/Tools/EGraph/ReducingCong.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,11 +415,11 @@ Section ReducingStep.
- rewrite (Hext _ _ Hgv); exact Hor.
- discriminate Hor. }
pose proof (@lang_model_ok V V_Eqb V_Eqb_ok sort_of l sort_of_fresh wfl) as Hmok.
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x1 eb i2 Hok_eb Hsnd_eb) as Hg1.
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x1 i2 eb Hok_eb Hsnd_eb) as Hg1.
rewrite Hga1 in Hg1; cbn [snd] in Hg1; destruct Hg1 as [Hok_e1 Hsnd_e1].
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x2 e1 i2 Hok_e1 Hsnd_e1) as Hg2.
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x2 i2 e1 Hok_e1 Hsnd_e1) as Hg2.
rewrite Hga2 in Hg2; cbn [snd] in Hg2; destruct Hg2 as [Hok_e2 Hsnd_e2].
pose proof (@rebuild_sound V V_Eqb V_Eqb_ok lt succ V_default V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok (option positive) (size V) lang_model Hmok (fun _ => True) rfuel e2 Hok_e2) as Hrbs.
pose proof (@rebuild_sound V V_Eqb V_Eqb_ok lt succ V_default V V_Eqb V_Eqb_ok V_map V_map_ok V_map V_map_ok V_trie V_trie_ok (option positive) (size V) lang_model Hmok rfuel e2 Hok_e2) as Hrbs.
rewrite Hrb in Hrbs; cbn [snd] in Hrbs; destruct Hrbs as [Hok_e3 Hiff3].
assert (Hsnd_e3 : sound i2 e3) by (apply (Hiff3 i2); exact Hsnd_e2).
match type of Hsat with
Expand All @@ -428,18 +428,18 @@ Section ReducingStep.
assert (HP : forall ee ii, egraph_ok ee -> sound ii ee -> egraph_ok (snd (pred ee)) /\ sound ii (snd (pred ee)))
by (intros ee ii Hoke Hsnde; subst pred; unfold weight_less_than;
cbn [Mbind Mret StateMonad.state_monad];
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x1 ee ii Hoke Hsnde) as Hp1;
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x1 ii ee Hoke Hsnde) as Hp1;
destruct (get_analysis V V V_map V_map V_trie (option positive) x1 ee) as [a1 e1'] eqn:He1';
cbn [snd] in Hp1; destruct Hp1 as [ Hok1 Hsnd1 ]; cbn [fst snd];
destruct (oP_lt a1 w1);
[ cbn [snd]; split; assumption | ];
cbn [fst snd];
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x2 e1' ii Hok1 Hsnd1) as Hp2;
pose proof (@get_analysis_preserves_ok_sound V lt V V_map V_map V_trie (option positive) (size V) lang_model x2 ii e1' Hok1 Hsnd1) as Hp2;
destruct (get_analysis V V V_map V_map V_trie (option positive) x2 e1') as [a2 e2'] eqn:He2';
cbn [snd] in Hp2; destruct Hp2 as [ Hok2 Hsnd2 ];
destruct (oP_lt a2 w2);
[ cbn [snd]; split; assumption | ];
pose proof (@are_unified_preserves_ok_sound V V_Eqb V_Eqb_ok lt succ V_default V V_map V_map V_map_ok V_trie (option positive) lang_model x1 x2 e2' ii Hok2 Hsnd2) as Hau;
pose proof (@are_unified_preserves_ok_sound V V_Eqb V_Eqb_ok lt succ V_default V V_map V_map V_map_ok V_trie (option positive) lang_model x1 x2 ii e2' Hok2 Hsnd2) as Hau;
destruct Hau as [ Hoku Hsndu ]; split; assumption).
pose proof (@scheduled_saturate_until_sound V V_Eqb V_Eqb_ok V_default V_map V_map_plus V_map_ok V_trie V_trie_ok succ V_leb lt lt_asymmetric lt_succ lt_trans V_map_plus_ok (option positive) (size V) spaced_list_intersect lang_model Hmok rfuel pred HP schedule Hsched sat_fuel i2 e3 Hok_e3 Hsnd_e3) as Hss.
rewrite Hsat in Hss.
Expand Down Expand Up @@ -779,7 +779,7 @@ Section CongMain.
assert (Hky : Sep.has_key y (parent (equiv g))) by (exact (interpretation_exact _ _ _ _ _ _ _ _ _ Hsndg y Hisy)).
destruct (are_unified x y g) as [unified pf] eqn:Hau.
destruct unified.
* pose proof (are_unified_eq_sound V V_Eqb V_Eqb_ok lt succ V_default V V_map V_map V_map_ok V_trie (option positive) lang_model x y g i Hokg Hsndg Hkx Hky ltac:(rewrite Hau; reflexivity)) as Hes.
* pose proof (are_unified_eq_sound V V_Eqb V_Eqb_ok lt succ V_default V V_map V_map V_map_ok V_trie (option positive) lang_model x y i g Hokg Hsndg Hkx Hky ltac:(rewrite Hau; reflexivity)) as Hes.
eapply (eq_sound_to_eq_term V V_map sort_of l sort_of_fresh wfl i x y e1 e2 Hes); [ exact Hr1 | exact Hr2 ].
* destruct (extract_weighted g efuel x) as [e1'|err1] eqn:Hex; cbn [Mbind Mret result_monad] in Hproc; [ | discriminate ].
destruct (extract_weighted g efuel y) as [e2'|err2] eqn:Hey; cbn [Mbind Mret result_monad] in Hproc; [ | discriminate ].
Expand Down
12 changes: 4 additions & 8 deletions src/Utils/EGraph/BuildTriesDepth.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,16 +61,12 @@ Section VariableFlags.
- inversion Hnd as [|? ? Hnotin Hnd']; subst.
cbn [filter variable_flags map].
destruct (p qx) eqn:Hp.
+ (* p qx = true *)
rewrite eqb_refl_true by exact Eqb_idx_ok.
+ rewrite eqb_refl_true by exact Eqb_idx_ok.
cbn. f_equal. apply IH. exact Hnd'.
+ (* p qx = false *)
destruct (filter p qv') as [|cx cvs'] eqn:Hf.
* (* filter p qv' = [] *)
cbn [variable_flags]. f_equal.
+ destruct (filter p qv') as [|cx cvs'] eqn:Hf.
* cbn [variable_flags]. f_equal.
rewrite IH; [| exact Hnd']. reflexivity.
* (* filter p qv' = cx :: cvs' *)
assert (Hcx_in : In cx qv'). {
* assert (Hcx_in : In cx qv'). {
assert (Hin : In cx (filter p qv')) by (rewrite Hf; left; reflexivity).
apply filter_In in Hin. apply Hin. }
assert (Hqx_ne_cx : qx <> cx). {
Expand Down
Loading