pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Improve robustness of set simplification

Browse source
This commit is contained in:
Adam Chlipala 2018-03-17 19:35:43 -04:00
parent c8cfde5acf
commit a48d85c84c
2 changed files with 20 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
FrapWithoutSets.v
View file

@ -159,8 +159,16 @@ Ltac removeDups :=
Ltac doSubtract := Ltac doSubtract :=
match goal with match goal with
| [ |- context[constant ?ls \setminus constant ?ls0] ] => | [ |- context[@minus ?A (@constant ?A1 ?ls) (@constant ?A2 ?ls0)] ] =>
erewrite (@doSubtract_ok _ ls ls0) match A with
| A1 => idtac
| _ => change (@constant A1 ls) with (@constant A ls)
end;
match A with
| A2 => idtac
| _ => change (@constant A2 ls0) with (@constant A ls0)
end;
erewrite (@doSubtract_ok A ls ls0)
by repeat (apply DsNil by repeat (apply DsNil
|| (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ]) || (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|| (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ])) || (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))

12
Sets.v
View file

@ -258,8 +258,16 @@ Ltac fancy_neq :=
Ltac doSubtract := Ltac doSubtract :=
match goal with match goal with
| [ |- context[constant ?ls \setminus constant ?ls0] ] => | [ |- context[@minus ?A (@constant ?A1 ?ls) (@constant ?A2 ?ls0)] ] =>
erewrite (@doSubtract_ok _ ls ls0) match A with
| A1 => idtac
| _ => change (@constant A1 ls) with (@constant A ls)
end;
match A with
| A2 => idtac
| _ => change (@constant A2 ls0) with (@constant A ls0)
end;
erewrite (@doSubtract_ok A ls ls0)
by repeat (apply DsNil by repeat (apply DsNil
|| (apply DsKeep; [ simpl; intuition (congruence || fancy_neq) | ]) || (apply DsKeep; [ simpl; intuition (congruence || fancy_neq) | ])
|| (apply DsDrop; [ simpl; intuition congruence | ])) || (apply DsDrop; [ simpl; intuition congruence | ]))