Skip to content
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

Adapt w.r.t. coq/coq#17564. #139

Merged
merged 1 commit into from
May 3, 2023
Merged

Adapt w.r.t. coq/coq#17564. #139

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
8 changes: 4 additions & 4 deletions core/PartialExtendedMapSimulations.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ Proof using name_map_bijective.
move => f h d.
apply functional_extensionality => n.
rewrite /update /=.
case (name_eq_dec _ _) => H_dec; case (name_eq_dec _ _) => H_dec' //.
case: (name_eq_dec _ _) => H_dec; case (name_eq_dec _ _) => H_dec' //.
- rewrite -H_dec in H_dec'.
by rewrite H_dec.
- case: H_dec'.
Expand Down Expand Up @@ -189,7 +189,7 @@ case => {net net' tr}.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case name_eq_dec => H_dec //.
case: name_eq_dec => H_dec //.
by rewrite H_dec H_d.
by rewrite H_eq_s.
- move => h net net' out inp d l H_hnd H_eq.
Expand Down Expand Up @@ -218,7 +218,7 @@ case => {net net' tr}.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case name_eq_dec => H_dec //.
case: name_eq_dec => H_dec //.
by rewrite H_dec H_d.
by rewrite H_eq_s.
Qed.
Expand Down Expand Up @@ -594,7 +594,7 @@ invcs H_step.
repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=.
* by find_apply_lem_hyp not_in_failed_not_in.
* by find_apply_lem_hyp in_failed_in.
* case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
* case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
+ by rewrite IH.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
Expand Down
18 changes: 9 additions & 9 deletions core/PartialMapSimulations.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ Proof using name_map_bijective.
move => f h d.
apply functional_extensionality => n.
rewrite /update /=.
case name_eq_dec => H_dec; case name_eq_dec => H_dec' //.
case: name_eq_dec => H_dec; case name_eq_dec => H_dec' //.
rewrite -H_dec in H_dec'.
by rewrite tot_map_name_inverse_inv in H_dec'.
rewrite H_dec' in H_dec.
Expand Down Expand Up @@ -274,7 +274,7 @@ case => {net net' tr}.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case (name_eq_dec _ _) => H_dec //.
case: (name_eq_dec _ _) => H_dec //.
by rewrite H_dec H_d.
by rewrite H_eq_s.
* move {H_eq'}.
Expand Down Expand Up @@ -308,7 +308,7 @@ case => {net net' tr}.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case (name_eq_dec _ _) => H_dec //.
case: (name_eq_dec _ _) => H_dec //.
by rewrite H_dec H_d.
by rewrite H_eq_s.
* rewrite /=.
Expand Down Expand Up @@ -408,7 +408,7 @@ invcs H_step.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case (name_eq_dec _ _) => H_dec //.
case: (name_eq_dec _ _) => H_dec //.
by rewrite H_dec.
by rewrite H_eq_s.
- rewrite /= /pt_map_net /=.
Expand All @@ -434,7 +434,7 @@ invcs H_step.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case (name_eq_dec _ _) => H_dec //.
case: (name_eq_dec _ _) => H_dec //.
by rewrite H_dec H_d.
by rewrite H_eq_s.
- case H_m: (pt_map_packet p) => [p'|].
Expand Down Expand Up @@ -849,7 +849,7 @@ Proof using.
move => m m' h.
elim => //=.
move => n ns IH.
case (adjacent_to_dec _ _) => H_dec /=; last exact: IH.
case: (adjacent_to_dec _ _) => H_dec /=; last exact: IH.
case => n' m0 H_eq.
rewrite /pt_map_name_msg /=.
case H_eq': (pt_map_msg m') => [m1|]; last by rewrite H_eq' in H_eq.
Expand Down Expand Up @@ -1242,7 +1242,7 @@ invcs H_step.
repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=.
* by find_apply_lem_hyp not_in_failed_not_in.
* by find_apply_lem_hyp in_failed_in.
* case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
* case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
+ by rewrite IH.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
Expand Down Expand Up @@ -1285,7 +1285,7 @@ invcs H_step.
rewrite /nwS1 /nwS2 {nwS1 nwS2}.
apply functional_extensionality => n.
rewrite /update /=.
case name_eq_dec => H_dec //.
case: name_eq_dec => H_dec //.
by rewrite H_dec H5 H_eq_d.
have H_eq_p: nwP1 = nwP2.
rewrite /nwP1 /nwP2 /=.
Expand Down Expand Up @@ -1330,7 +1330,7 @@ invcs H_step.
rewrite /nwS1 /nwS2 /=.
apply functional_extensionality => n.
rewrite /update /=.
case name_eq_dec => H_dec //.
case: name_eq_dec => H_dec //.
by rewrite H_dec H5 H_d.
by rewrite H_eq_n.
- left.
Expand Down
10 changes: 5 additions & 5 deletions core/TotalMapSimulations.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -867,7 +867,7 @@ Proof using.
move => h m.
elim => //=.
move => n ns IH.
case (adjacent_to_dec _ _) => H_dec /=.
case: (adjacent_to_dec _ _) => H_dec /=.
case => n' m' H_in.
case: H_in => H_in.
by inversion H_in.
Expand Down Expand Up @@ -994,7 +994,7 @@ elim => //= [|n l IH] failed h n'; first by rewrite remove_all_nil.
have H_cn := remove_all_cons name_eq_dec failed n l.
break_or_hyp; break_and; find_rewrite; first exact: IH.
rewrite /=.
case (adjacent_to_dec _ _) => H_dec' /=.
case: (adjacent_to_dec _ _) => H_dec' /=.
move => H_in.
case: H_in => H_in.
inversion H_in.
Expand All @@ -1013,7 +1013,7 @@ elim => [|n l IH] failed n' h; first by rewrite remove_all_nil.
have H_cn := remove_all_cons name_eq_dec failed n l.
break_or_hyp; break_and; find_rewrite; first exact: IH.
rewrite /=.
case (adjacent_to_dec _ _) => /= H_dec'.
case: (adjacent_to_dec _ _) => /= H_dec'.
move => H_in.
case: H_in => H_in.
rewrite {1}H_in -{4}H_in.
Expand Down Expand Up @@ -1161,7 +1161,7 @@ Proof using.
move => m.
elim => //=.
move => n ns IH n' h H_adj H_in.
case (adjacent_to_dec _ _) => H_dec; case: H_in => H_in.
case: (adjacent_to_dec _ _) => H_dec; case: H_in => H_in.
- rewrite /=.
left.
by rewrite H_in.
Expand Down Expand Up @@ -1572,7 +1572,7 @@ invcs H_step.
repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=.
* by find_apply_lem_hyp not_in_failed_not_in.
* by find_apply_lem_hyp in_failed_in.
* case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
* case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=.
+ by rewrite IH.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
+ by find_apply_lem_hyp tot_adjacent_to_fst_snd.
Expand Down