diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/spl/Assumptions.v | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/spl/Assumptions.v')
| -rw-r--r-- | src/spl/Assumptions.v | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/spl/Assumptions.v b/src/spl/Assumptions.v index 1f2bb93..b3dee4b 100644 --- a/src/spl/Assumptions.v +++ b/src/spl/Assumptions.v @@ -68,7 +68,7 @@ Section Checker. End Forallb2. - Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) := + Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) : C.t := if forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem then concl else C._true. @@ -107,6 +107,18 @@ Section Checker_correct. rewrite <- (interp_check_clause _ _ H). now apply Hs. Qed. + Lemma valid_check_forall_inst (lemma : Prop) : + lemma -> + forall concl, + (lemma -> interp_uf rho concl) -> + C.valid rho concl. + + Proof. + intros pl concl applemma. + unfold C.valid. rewrite interp_equiv. + now apply applemma. + Qed. + Variable prem_id : list int. Variable prem : list C.t. Variable concl : C.t. @@ -123,10 +135,7 @@ Section Checker_correct. - now apply C.interp_true. - case_eq (forallb2 (fun i j => i == j) (S.get s pid) (S.sort_uniq p)); simpl; intro Heq; [ |now apply C.interp_true]. - case_eq (forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) pids ps); - simpl; intro Heq2; [ |now apply C.interp_true]. - assert (IH:=IHpids _ (H (valid_check_clause _ _ Heq))). - now rewrite Heq2 in IH. + apply IHpids. apply H. apply (valid_check_clause _ _ Heq). Qed. End Checker_correct. |