pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-03-19 11:12:28 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fixed to work in Coq 8.4, too

Browse source
This commit is contained in:
Adam Chlipala 2016-02-18 17:51:58 -05:00
parent cf65c18ebf
commit 2c601b04a0
3 changed files with 20 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Frap.v
View file

@ -43,7 +43,11 @@ Ltac invert0 e := invert e; fail.
Ltac invert1 e := invert0 e || (invert e; []). Ltac invert1 e := invert0 e || (invert e; []).
Ltac invert2 e := invert1 e || (invert e; [|]). Ltac invert2 e := invert1 e || (invert e; [|]).
Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *; repeat unifyTails); Ltac simplify := repeat (unifyTails; pose proof I);
repeat match goal with
| [ H : True |- _ ] => clear H
end;
repeat progress (simpl in *; intros; try autorewrite with core in *);
repeat (removeDups || doSubtract). repeat (removeDups || doSubtract).
Ltac propositional := intuition idtac. Ltac propositional := intuition idtac.

2
ModelChecking.v
View file

@ -248,7 +248,7 @@ Ltac model_check_infer :=
apply multiStepClosure_ok; simplify; model_check_steps. apply multiStepClosure_ok; simplify; model_check_steps.
Ltac model_check_find_invariant := Ltac model_check_find_invariant :=
simplify; eapply invariant_weaken; [ model_check_infer | ]. simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
Ltac model_check := model_check_find_invariant; model_check_finish. Ltac model_check := model_check_find_invariant; model_check_finish.

13
Sets.v
View file

@ -169,9 +169,22 @@ Proof.
unfold constant; intuition eauto using removeDups_fwd, removeDups_bwd. unfold constant; intuition eauto using removeDups_fwd, removeDups_bwd.
Qed. Qed.
Ltac someMatch ls :=
match ls with
| ?x :: ?ls' =>
let rec someMatch' ls :=
match ls with
| x :: _ => idtac
| _ :: ?ls' => someMatch' ls'
end
in someMatch' ls'
| _ :: ?ls' => someMatch ls'
end.
Ltac removeDups := Ltac removeDups :=
match goal with match goal with
| [ |- context[constant ?ls] ] => | [ |- context[constant ?ls] ] =>
someMatch ls;
erewrite (@removeDups_ok _ ls) erewrite (@removeDups_ok _ ls)
by repeat (apply RdNil by repeat (apply RdNil
|| (apply RdNew; [ simpl; intuition congruence | ]) || (apply RdNew; [ simpl; intuition congruence | ])