Skip to content

Adapt to rocq-prover/rocq#21987 (secvar status) #2334

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

Merged
JasonGross merged 1 commit into from
May 28, 2026
Merged

Adapt to rocq-prover/rocq#21987 (secvar status) #2334

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
26 changes: 13 additions & 13 deletions src/Util/FSets/FMapTrie.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1119,11 +1119,11 @@ Module Import ListWSfun_gen_proofs.
Proof using Type.
clear.
cbv [MapsTo find].
destruct m as [m' pf]; cbn [proj1_sig]; clear m pf.
destruct (m) as [m' pf]; cbn [proj1_sig]; clear m pf.
revert x y m'.
induction x as [|x' xs IH], y as [|y' ys], m' as [m|]; clear x y m';
induction x as [|x' xs IH], y as [|y' ys], m' as [m|]; try clear x y m';
try specialize (IH ys);
try (induction m as [d m'] using (t_case (elt:=elt)); clear m).
try (induction m as [d m'] using (t_case (elt:=elt)); try clear m).
all: t.
all: pose_MapsTo_as_find M.MapsTo_1.
all: repeat match goal with
Expand Down Expand Up @@ -1157,7 +1157,7 @@ Module Import ListWSfun_gen_proofs.
cbv [elements elements_with_key_prefix_and fold'].
rewrite <- rev_alt; destruct m0 as [m'|]; [ | rewrite rev_involutive; reflexivity ].
revert i k_prefix.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); clear m'; intros.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); try clear m'; intros.
repeat (autounfold with trie_db; autorewrite with trie_db).
destruct m; try (now destruct d; cbn [List.rev]; rewrite rev_involutive); [].
rewrite !M.fold_1.
Expand Down Expand Up @@ -1190,7 +1190,7 @@ Module Import ListWSfun_gen_proofs.
destruct m0 as [m'|]; [ | now rewrite ?app_nil_r ].
generalize (List.rev prefix); clear prefix; intro prefix.
revert prefix k_prefix.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); clear m'; intros.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); try clear m'; intros.
repeat (autounfold with trie_db; autorewrite with trie_db).
destruct m; try (now destruct d; rewrite ?app_nil_r, ?app_nil_l); [].
rewrite !M.fold_1.
Expand Down Expand Up @@ -1250,7 +1250,7 @@ Module Import ListWSfun_gen_proofs.
rewrite elements_alt_1.
cbv [fold'].
destruct m0 as [m'|]; [ | now rewrite ?app_nil_r ].
induction m' as [d m pf] using (t_case (elt:=elt)); clear m'.
induction m' as [d m pf] using (t_case (elt:=elt)); try clear m'.
repeat (autounfold with trie_db; autorewrite with trie_db).
destruct m as [m'|]; [ | break_innermost_match; cbn; now rewrite ?app_nil_r ].
cbn [List.app].
Expand Down Expand Up @@ -1288,7 +1288,7 @@ Module Import ListWSfun_gen_proofs.
clearbody i k_prefix'.
clear.
revert k_prefix k_prefix'.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); clear m'; intros.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); try clear m'; intros.
repeat (autounfold with trie_db; autorewrite with trie_db).
destruct m as [m'|]; [ | break_innermost_match; cbn; now rewrite ?app_nil_r ].
rewrite map_app.
Expand Down Expand Up @@ -1331,7 +1331,7 @@ Module Import ListWSfun_gen_proofs.
change (@nil ?A) with (List.rev (@nil A)) at 2.
rewrite elements_with_key_prefix_alt; cbn -[elements'].
destruct m0 as [m'|]; [ | reflexivity ].
induction m' as [d m pf] using (t_case (elt:=elt)); clear m'.
induction m' as [d m pf] using (t_case (elt:=elt)); try clear m'.
repeat (autounfold with trie_db; autorewrite with trie_db).
repeat (f_equiv; []; repeat intro).
break_innermost_match.
Expand All @@ -1348,7 +1348,7 @@ Module Import ListWSfun_gen_proofs.
destruct m as [[m'|] pf']; clear m; [ | reflexivity ].
cbn [proj1_sig] in *; clear pf'.
revert f i.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); clear m'; intros.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); try clear m'; intros.
rewrite elements'_alt.
repeat (autounfold with trie_db; autorewrite with trie_db).
destruct m as [m'|]; [ | now break_innermost_match ].
Expand All @@ -1369,7 +1369,7 @@ Module Import ListWSfun_gen_proofs.
revert x' y' m0.
induction x' as [|x xs IH], y' as [|y ys], m0 as [m|];
first [ specialize (IH ys) | try clear IH ];
try (induction m as [d m'] using (t_case (elt:=elt)); clear m).
try (induction m as [d m'] using (t_case (elt:=elt)); try clear m).
all: repeat first [ progress invlist eqlistA
| progress cbn [find' add' Option.bind]
| progress cbv [not] in *
Expand Down Expand Up @@ -1398,7 +1398,7 @@ Module Import ListWSfun_gen_proofs.
revert x' y' m0.
induction x' as [|x xs IH], y' as [|y ys], m0 as [m|];
first [ specialize (IH ys) | try clear IH ];
try (induction m as [d m'] using (t_case (elt:=elt)); clear m).
try (induction m as [d m'] using (t_case (elt:=elt)); try clear m).
all: repeat first [ progress intros
| progress subst
| progress inversion_option
Expand Down Expand Up @@ -1457,7 +1457,7 @@ Module Import ListWSfun_gen_proofs.
cbv [find elements proj1_sig]; clear pf; rename m' into m.
revert m; induction x as [|?? IH];
(intros [m'|];
[ induction m' as [d m pf] using (t_case (elt:=elt)); clear m'
[ induction m' as [d m pf] using (t_case (elt:=elt)); try clear m'
| now rewrite elements'_alt; destruct x; cbn; split; intros; inversion_option; firstorder ]).
all: rewrite elements'_alt.
all: repeat (autounfold with trie_db; autorewrite with trie_db).
Expand Down Expand Up @@ -1511,7 +1511,7 @@ Module Import ListWSfun_gen_proofs.
clear.
cbv [elements proj1_sig]; destruct m as [[m'|] _]; clear m;
[ | now constructor ].
induction m' as [d m pf IH] using (t_ind (elt:=elt)); clear m'.
induction m' as [d m pf IH] using (t_ind (elt:=elt)); try clear m'.
rewrite elements'_alt.
repeat (autounfold with trie_db; autorewrite with trie_db).
apply NoDupA_app; try exact _; break_innermost_match; repeat constructor;
Expand Down
Loading