Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 0a279daf authored by BESSON Frederic's avatar BESSON Frederic
Browse files

Fix coq 8.14

parent 08d06d8a
No related branches found
Tags 8.14.0
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Makefile
+ 0
− 1
View file @ 0a279daf
......@@ -10,7 +10,6 @@ ifneq (,$(COQBIN))
COQBIN:=$(COQBIN)/
endif
all : theories/Itauto.vo theories/NOlia.vo theories/NOlra.vo
theories/Prover.vo src/prover.ml : CoqMakefile
......
_CoqProject
+ 3
− 1
View file @ 0a279daf
......@@ -5,4 +5,6 @@ theories/PatriciaR.v
theories/KeyInt.v
theories/Formula.v
theories/Prover.v
theories/ZArithDec.v
theories/NOlia.v
theories/NOlra.v
opam
+ 1
− 1
View file @ 0a279daf
......@@ -14,7 +14,7 @@ install: [
]
depends: [
"ocaml" {>= "4.9~" & < "4.13~"}
"coq" {>= "8.13.~" }
"coq" {>= "8.14.~" }
"ocamlbuild" {build }
]
depopts: [ "ocamlformat" {build} ]
......
paper/itauto-slides.tex
+ 415
− 247
View file @ 0a279daf
This diff is collapsed.
test-suite/arith.v
+ 5
− 5
View file @ 0a279daf
......@@ -44,17 +44,17 @@ Proof.
Qed.
Instance Zge_dec : DecP2 Z.ge.
#[local] Instance Zge_dec : DecP2 Z.ge.
Proof.
unfold DecP2. intros. lia.
Qed.
Instance Zle_dec : DecP2 Z.le.
#[local] Instance Zle_dec : DecP2 Z.le.
Proof.
unfold DecP2. intros. lia.
Qed.
Instance Zeq_dec : DecP2 (@eq Z).
#[local] Instance Zeq_dec : DecP2 (@eq Z).
Proof.
unfold DecP2. intros. lia.
Qed.
......@@ -199,14 +199,14 @@ Require Import Bool.
Open Scope bool_scope.
Require Import ZifyClasses.
Program Instance Op_eq_bool : BinRel (@eq bool) :=
#[local] Program Instance Op_eq_bool : BinRel (@eq bool) :=
{TR := fun x y => Is_true (implb x y) /\ Is_true (implb y x) ; TRInj := _ }.
Next Obligation.
destruct n,m; simpl; intuition congruence.
Qed.
Add Zify BinRel Op_eq_bool.
Program Instance Op_negb : UnOp negb :=
#[local] Program Instance Op_negb : UnOp negb :=
{TUOp := fun x => implb x false ; TUOpInj:= _ }.
Add Zify UnOp Op_negb.
......
test-suite/refl_bool.v
+ 2
− 2
View file @ 0a279daf
......@@ -8,8 +8,8 @@ Proof.
destruct (a <=? b); intuition congruence.
Qed.
Instance leb_le : Reflect.Rbool2 leb := Reflect.mkrbool2 _ _ leb le is_true_le.
Instance le_leb : Reflect.RProp2 le := Reflect.mkrProp2 _ _ le leb is_true_le.
#[local] Instance leb_le : Reflect.Rbool2 leb := Reflect.mkrbool2 _ _ leb le is_true_le.
#[local] Instance le_leb : Reflect.RProp2 le := Reflect.mkrProp2 _ _ le leb is_true_le.
Require Import Cdcl.Itauto.
Require Import Int63.
......
theories/Formula.v
+ 27
− 27
View file @ 0a279daf
(* Copyright 2020 Frédéric Besson <frederic.besson@inria.fr> *)
Require Import Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Coqlib.
Require Import Bool Setoid ZifyBool ZArith Int63 Lia List.
Require Import Bool Setoid ZifyBool ZArith Uint63 Lia List.
Import ZifyClasses.
Set Primitive Projections.
......@@ -38,54 +38,54 @@ Ltac destruct_in_hyp H eqn :=
end.
Lemma compare_refl : forall i, (i ?= i)%int63 = Eq.
Lemma compare_refl : forall i, (i ?= i)%uint63 = Eq.
Proof.
intros.
rewrite compare_def_spec.
unfold compare_def.
replace (i <? i)%int63 with false by lia.
replace (i =? i)%int63 with true by lia.
replace (i <? i)%uint63 with false by lia.
replace (i =? i)%uint63 with true by lia.
reflexivity.
Qed.
Lemma compare_Eq : forall x y, (x ?= y)%int63 = Eq <-> (x =? y = true)%int63.
Lemma compare_Eq : forall x y, (x ?= y)%uint63 = Eq <-> (x =? y = true)%uint63.
Proof.
intros.
rewrite compare_def_spec.
unfold compare_def.
destruct (x <?y)%int63 eqn:LT; try congruence.
destruct (x <?y)%uint63 eqn:LT; try congruence.
intuition (congruence || lia).
destruct (x =?y)%int63 ; intuition (congruence || lia).
destruct (x =?y)%uint63 ; intuition (congruence || lia).
Qed.
Lemma compare_Lt : forall x y, (x ?= y)%int63 = Lt <-> (x <? y = true)%int63.
Lemma compare_Lt : forall x y, (x ?= y)%uint63 = Lt <-> (x <? y = true)%uint63.
Proof.
intros.
rewrite compare_def_spec.
unfold compare_def.
destruct (x <?y)%int63 eqn:LT; try congruence.
destruct (x <?y)%uint63 eqn:LT; try congruence.
intuition (congruence || lia).
destruct (x =?y)%int63 ; intuition (congruence || lia).
destruct (x =?y)%uint63 ; intuition (congruence || lia).
Qed.
Lemma compare_Gt : forall x y, (x ?= y)%int63 = Gt <-> (y <? x = true)%int63.
Lemma compare_Gt : forall x y, (x ?= y)%uint63 = Gt <-> (y <? x = true)%uint63.
Proof.
intros.
rewrite compare_def_spec.
unfold compare_def.
destruct (x <?y)%int63 eqn:LT; try congruence.
destruct (x <?y)%uint63 eqn:LT; try congruence.
intuition (congruence || lia).
destruct (x =?y)%int63 eqn:EQ; intuition (congruence || lia).
destruct (x =?y)%uint63 eqn:EQ; intuition (congruence || lia).
Qed.
Ltac elim_compare :=
match goal with
| H : (?X ?= ?Y)%int63 = Eq |- _ => rewrite compare_Eq in H
| H : (?X ?= ?Y)%int63 = Lt |- _ => rewrite compare_Lt in H
| H : (?X ?= ?Y)%int63 = Gt |- _ => rewrite compare_Gt in H
| |- (?X ?= ?Y)%int63 = Eq => rewrite compare_Eq
| |- (?X ?= ?Y)%int63 = Lt => rewrite compare_Lt
| |- (?X ?= ?Y)%int63 = Gt => rewrite compare_Gt
| H : (?X ?= ?Y)%uint63 = Eq |- _ => rewrite compare_Eq in H
| H : (?X ?= ?Y)%uint63 = Lt |- _ => rewrite compare_Lt in H
| H : (?X ?= ?Y)%uint63 = Gt |- _ => rewrite compare_Gt in H
| |- (?X ?= ?Y)%uint63 = Eq => rewrite compare_Eq
| |- (?X ?= ?Y)%uint63 = Lt => rewrite compare_Lt
| |- (?X ?= ?Y)%uint63 = Gt => rewrite compare_Gt
end.
Lemma lift_if : forall (P: bool -> Prop), forall x, (x = true -> P true) /\ (x = false -> P false) -> P x.
......@@ -132,7 +132,7 @@ Module HCons.
destruct f ; reflexivity.
Qed.
Definition eq_hc (f1 f2 : t) := (id f1 =? id f2)%int63 && Bool.eqb (is_dec f1) (is_dec f2).
Definition eq_hc (f1 f2 : t) := (id f1 =? id f2)%uint63 && Bool.eqb (is_dec f1) (is_dec f2).
End S.
......@@ -186,7 +186,7 @@ Qed.
constructor.
Qed.
Hint Resolve wf_map_add : wf.
#[local] Hint Resolve wf_map_add : wf.
Lemma wf_map_remove :
forall {A: Type} x
......@@ -198,7 +198,7 @@ Qed.
apply IntMap.wf_remove'; auto.
Qed.
Hint Resolve wf_map_remove : wf.
#[local] Hint Resolve wf_map_remove : wf.
Inductive op :=
......@@ -240,7 +240,7 @@ Inductive op :=
List.fold_right (fun e acc => max (Depth e.(elt)) acc) O l.
Lemma in_max_elt : forall l x (IN: In x l),
Depth (elt x) < S(max_list l).
(Depth (elt x) < S(max_list l))%nat.
Proof.
induction l; simpl ; auto.
- tauto.
......@@ -395,7 +395,7 @@ Inductive op :=
Proof. destruct f ; reflexivity. Qed.
Open Scope int63.
Open Scope uint63.
......@@ -1128,7 +1128,7 @@ Inductive op :=
destruct (is_positive_literal l); auto with wf.
Qed.
Hint Resolve wf_map_add_clause_old : wf.
#[local] Hint Resolve wf_map_add_clause_old : wf.
Lemma wf_map_add_clause :
forall l id cl cls
......@@ -2510,13 +2510,13 @@ Inductive op :=
* firstorder.
* firstorder.
* firstorder congruence.
apply 0%int63. (* ?? *)
apply 0%uint63. (* ?? *)
+ simpl.
intuition subst.
firstorder.
firstorder.
firstorder congruence.
apply 0%int63. (* ?? *)
apply 0%uint63. (* ?? *)
Qed.
......
theories/KeyInt.v
+ 119
− 119
View file @ 0a279daf
This diff is collapsed.
theories/NOlia.v
+ 5
− 5
View file @ 0a279daf
......@@ -6,25 +6,25 @@ Record ZarithThy : Type.
(** Get the theory from zify *)
Instance CstOpThy (S T: Type) (I : InjTyp S T) (C: S) (COp : @CstOp S T C I) :
#[export] Instance CstOpThy (S T: Type) (I : InjTyp S T) (C: S) (COp : @CstOp S T C I) :
TheorySig ZarithThy C := {}.
Instance UnOpThy (S1 S2 T1 T2: Type)
#[export] Instance UnOpThy (S1 S2 T1 T2: Type)
(I1 : InjTyp S1 T1) (I2 : InjTyp S2 T2)
(unop : S1 -> S2)
(UOp : @UnOp S1 S2 T1 T2 unop I1 I2) :
TheorySig ZarithThy unop := {}.
Instance BinOpThy (S1 S2 S3 T1 T2 T3: Type)
#[export] Instance BinOpThy (S1 S2 S3 T1 T2 T3: Type)
(I1 : InjTyp S1 T1) (I2 : InjTyp S2 T2)
(I3 : InjTyp S3 T3)
(binop : S1 -> S2 -> S3)
(BOp : @BinOp S1 S2 S3 T1 T2 T3 binop I1 I2 I3) :
TheorySig ZarithThy binop := {}.
Instance BinRelThy (S T: Type) (I: InjTyp S T) (R: S -> S -> Prop)
#[export] Instance BinRelThy (S T: Type) (I: InjTyp S T) (R: S -> S -> Prop)
(BR : @BinRel S T R I) : TheorySig ZarithThy R := {}.
Instance InjTypThy (S T: Type) (I: InjTyp S T) : TheoryType ZarithThy S := {}.
#[export] Instance InjTypThy (S T: Type) (I: InjTyp S T) : TheoryType ZarithThy S := {}.
Ltac smt := itauto (no ZarithThy congruence lia).
theories/NOlra.v
+ 18
− 18
View file @ 0a279daf
......@@ -4,27 +4,27 @@ Require Import ZifyClasses Lra Reals.
Record RarithThy : Type.
Instance RThy : TheoryType RarithThy R := {}.
#[export] Instance RThy : TheoryType RarithThy R := {}.
Instance R0Thy : TheorySig RarithThy R0 := {}.
Instance R1Thy : TheorySig RarithThy R1 := {}.
Instance RplusThy : TheorySig RarithThy Rplus := {}.
Instance RminusThy : TheorySig RarithThy Rminus := {}.
Instance RmultThy : TheorySig RarithThy Rmult := {}.
Instance IZRThy : TheorySig RarithThy IZR := {}.
Instance ReqThy : TheorySig RarithThy (@eq R) := {}.
Instance RltThy : TheorySig RarithThy Rlt := {}.
Instance RleThy : TheorySig RarithThy Rle := {}.
Instance RgeThy : TheorySig RarithThy Rge := {}.
Instance RgtThy : TheorySig RarithThy Rgt := {}.
#[export] Instance R0Thy : TheorySig RarithThy R0 := {}.
#[export] Instance R1Thy : TheorySig RarithThy R1 := {}.
#[export] Instance RplusThy : TheorySig RarithThy Rplus := {}.
#[export] Instance RminusThy : TheorySig RarithThy Rminus := {}.
#[export] Instance RmultThy : TheorySig RarithThy Rmult := {}.
#[export] Instance IZRThy : TheorySig RarithThy IZR := {}.
#[export] Instance ReqThy : TheorySig RarithThy (@eq R) := {}.
#[export] Instance RltThy : TheorySig RarithThy Rlt := {}.
#[export] Instance RleThy : TheorySig RarithThy Rle := {}.
#[export] Instance RgeThy : TheorySig RarithThy Rge := {}.
#[export] Instance RgtThy : TheorySig RarithThy Rgt := {}.
(* Integer constant are also part of theory *)
Instance Z0Thy : TheorySig RarithThy Z0 := {}.
Instance ZposThy : TheorySig RarithThy Zpos := {}.
Instance ZnegThy : TheorySig RarithThy Zneg := {}.
Instance xHThy : TheorySig RarithThy xH := {}.
Instance xIThy : TheorySig RarithThy xI := {}.
Instance xOThy : TheorySig RarithThy xO := {}.
#[export] Instance Z0Thy : TheorySig RarithThy Z0 := {}.
#[export] Instance ZposThy : TheorySig RarithThy Zpos := {}.
#[export] Instance ZnegThy : TheorySig RarithThy Zneg := {}.
#[export] Instance xHThy : TheorySig RarithThy xH := {}.
#[export] Instance xIThy : TheorySig RarithThy xI := {}.
#[export] Instance xOThy : TheorySig RarithThy xO := {}.
Ltac smt := itauto (no RarithThy congruence lra).
theories/ZArithDec.v
+ 6
− 6
View file @ 0a279daf
......@@ -44,17 +44,17 @@ Qed.
Instance DecLe : DecP2 Z.le := dec_le.
Instance DecLt : DecP2 Z.lt := dec_lt.
Instance DecGt : DecP2 Z.gt := dec_gt.
Instance DecGe : DecP2 Z.ge := dec_ge.
Instance DecEq : DecP2 (@eq Z) := dec_eq.
#[export] Instance DecLe : DecP2 Z.le := dec_le.
#[export] Instance DecLt : DecP2 Z.lt := dec_lt.
#[export] Instance DecGt : DecP2 Z.gt := dec_gt.
#[export] Instance DecGe : DecP2 Z.ge := dec_ge.
#[export] Instance DecEq : DecP2 (@eq Z) := dec_eq.
(** To eliminate literals of the form ~ x = y,
we generate the clause x < y \/ x = y \/ y < x.
*)
Instance negeqZ : TheoryPropagation.NegBinRel (@eq Z) :=
#[export] Instance negeqZ : TheoryPropagation.NegBinRel (@eq Z) :=
{
neg_bin_rel_clause := fun x y => x < y \/ x = y \/ y < x;
neg_bin_rel_correct := Z.lt_trichotomy
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment