# Definition of the datastructure

Require Export Cong.
Require Export List.
Require Export ZArith.
Require Export Bool.
Require Import ROmega.
Require Export Classical_Prop.
Require Import Zdivides.
Require Import ZArithRing.
Require Export Nat.

Expresssion
• Numbers
• Variables
• - deBrujn indices are used for variables and binders
Inductive exp : Set :=
| Num : natexp
| Var : natexp
| Plus : expexpexp.

Formulae :
• Quantifiers (Forall, Exists)
• Connectors (And,Or,Impl,Neg)
• Constants (True,False)
• Expressions (Eq,Cong)
Inductive form : Set :=
| Forall : formform
| Exists : formform
| ANd : formformform
| Or : formformform
| Imp : formformform
| Neg : formform
| TRue : form
| FAlse : form
| Eq : expexpform
| Cong : natexpexpform.

Define n.e as e+(n-1).e
Fixpoint scal (n : nat) : expexp :=
fun e
match n with
| ONum 0
| S Oe
| S nPlus e (scal n e)
end.

The semantic of expressions:
• the list l gives the value of the variables (deBrujn indices)
Fixpoint exp2Z (l : list Z) (a : exp) {struct a} : Z :=
match a with
| Plus b c ⇒ (exp2Z l b + exp2Z l c)%Z
| Num nZ_of_nat n
| Var nnth n l 0%Z
end.

i.a has the expected semantics
Theorem scal_correct :
i a l, exp2Z l (scal i a) = (Z_of_nat i × exp2Z l a)%Z.
intros i a l; elim i; auto.
intros n H; apply trans_equal with (exp2Z l a + exp2Z l (scal n a))%Z.
simpl in |- *; auto.
destruct n; simpl; try ring.
rewrite H; rewrite Znat.inj_S; ring.
Qed.

The semantic of formulae
Fixpoint form2Prop (l : list Z) (a : form) {struct a} : Prop :=
match a with
| Forall b x : Z, form2Prop (x :: l) b
| Exists b x : Z, form2Prop (x :: l) b
| ANd b cform2Prop l b form2Prop l c
| Or b cform2Prop l b form2Prop l c
| Imp b cform2Prop l bform2Prop l c
| Neg b¬ form2Prop l b
| TRueTrue
| FAlseFalse
| Form.Eq b cexp2Z l b = exp2Z l c
| Cong i b ccongZ i (exp2Z l b) (exp2Z l c)
end.

A little example
Eval compute in (form2Prop nil (Exists (Form.Eq (Var 0) (Num 0)))).

Build a conjunction from a list of formulae
Fixpoint buildConj (l : list form) : form :=
match l with
| nilTRue
| e :: nile
| e :: l1ANd e (buildConj l1)
end.
Property of buildConj
Theorem buildConj_append :
l l1 l2,
form2Prop l (buildConj (l1 ++ l2))
form2Prop l (buildConj l1) form2Prop l (buildConj l2).
intros l l1; elim l1; auto.
simpl in |- *; intuition.
intros a l1' Rec l2.
apply iff_trans with (form2Prop l a form2Prop l (buildConj (l1' ++ l2))).
simpl in |- *; case (l1' ++ l2); simpl in |- *; intuition.
apply
iff_trans
with
(form2Prop l a
form2Prop l (buildConj l1') form2Prop l (buildConj l2)).
simpl in |- *; generalize (Rec l2); intuition.
simpl in |- *; case l1'; simpl in |- *; intuition.
Qed.

Properties of form2Prop
Theorem form2Prop_cons :
a l l1,
form2Prop l1 a
form2Prop l1 (buildConj l) → form2Prop l1 (buildConj (a :: l)).
intros a l l1 H; simpl in |- *; case l; simpl in |- *; auto.
Qed.
Hint Resolve form2Prop_cons.

Theorem form2Prop_app :
l l1 l2,
form2Prop l (buildConj l1) →
form2Prop l (buildConj l2) → form2Prop l (buildConj (l1 ++ l2)).
intros l l1; elim l1; auto.
intros a l0 H l2 H0 H1;
change (form2Prop l (buildConj (a :: l0 ++ l2))) in |- *;
auto.
apply form2Prop_cons; auto.
generalize H0; case l0; simpl in |- *; auto; intuition.
apply H; auto; generalize H0; case l0; simpl in |- *; auto; intuition.
Qed.
Hint Resolve form2Prop_app.

Theorem form2Prop_cons_inv :
a l l1,
form2Prop l1 (buildConj (a :: l)) →
form2Prop l1 a form2Prop l1 (buildConj l).
intros a l l1; simpl in |- *; case l; simpl in |- *; auto.
Qed.

Theorem form2Prop_app_inv :
l l1 l2,
form2Prop l (buildConj (l1 ++ l2)) →
form2Prop l (buildConj l1) form2Prop l (buildConj l2).
intros l l1; elim l1; auto.
simpl in |- *; auto.
intros a l0 H l2 H0.
case (form2Prop_cons_inv a (l0 ++ l2) l); auto.
intros H1 H2; case (H l2); auto.
Qed.

Same as form2Prop but for a list of formulae

Fixpoint formL2Prop (c : Z) (l : list Z) (l1 : list (nat × form)) {struct l1}
: Prop :=
match l1 with
| (n, Form.Eq a b) :: l2
exp2Z l a = (c × Z_of_nat n + exp2Z l b)%Z formL2Prop c l l2
| (n, Neg (Form.Eq a b)) :: l2
exp2Z l a (c × Z_of_nat n + exp2Z l b)%Z formL2Prop c l l2
| (n, Cong i a b) :: l2
congZ i (exp2Z l a) (c × Z_of_nat n + exp2Z l b) formL2Prop c l l2
| nilTrue
| _False
end.

Property of formL2Prop

Theorem formL2Prop_append :
a l l1 l2,
formL2Prop a l (l1 ++ l2) formL2Prop a l l1 formL2Prop a l l2.
intros a l l1; elim l1; auto.
simpl in |- *; intuition.
intros b l1' Rec l2; simpl in |- *; case b; intros n f; case f;
try (intuition; fail).
intros f0; case f0; try (intuition; fail).
intros e1 e2; generalize (Rec l2); intuition.
intros e1 e2; generalize (Rec l2); intuition.
intros i e1 e2; generalize (Rec l2); intuition.
Qed.

Ground expression i.e. it contains no variable
Inductive groundExp : expProp :=
| GNum : i : nat, groundExp (Num i)
| GPlus :
a b : exp, groundExp agroundExp bgroundExp (Plus a b).

Ground formula i.e. it contains no variable
Inductive groundForm : formProp :=
| GTrue : groundForm TRue
| GFalse : groundForm FAlse
| GNeg : a : form, groundForm agroundForm (Neg a)
| GAnd :
a b : form, groundForm agroundForm bgroundForm (ANd a b)
| GOr :
a b : form, groundForm agroundForm bgroundForm (Or a b)
| GImp :
a b : form, groundForm agroundForm bgroundForm (Imp a b)
| GEq :
a b : exp,
groundExp agroundExp bgroundForm (Form.Eq a b)
| GCong :
(i : nat) (a b : exp),
groundExp agroundExp bgroundForm (Cong i a b).

A ground expression can be evaluated in an empty context
Theorem exp2Z_ground :
(l : list Z) (e : exp), groundExp eexp2Z nil e = exp2Z l e.
intros l e H; elim H; simpl in |- *; auto.
intros a b H0 H1 H2 H3; rewrite H1; rewrite H3; auto.
Qed.

An algorithm to decide ground formulae
• Take a formula that is known to be ground
• Returns a boolean
Fixpoint decideGround (a : form) : bool :=
match a with
| Forall bfalse
| Exists bfalse
| ANd b cdecideGround b && decideGround c
| Or b cdecideGround b || decideGround c
| Imp b cimplb (decideGround b) (decideGround c)
| Neg bnegb (decideGround b)
| TRuetrue
| FAlsefalse
| Form.Eq b cZ_eq_bool (exp2Z nil b) (exp2Z nil c)
| Cong i b c
match congZ_dec i (exp2Z nil b) (exp2Z nil c) with
| left _true
| _false
end
end.

decideGround is correct and complete on ground formulae
Theorem decideCorrect :
f : form,
groundForm f
match decideGround f with
| trueform2Prop nil f
| false¬ form2Prop nil f
end.
intros f H; elim H; simpl in |- *; try (intros; discriminate); auto.
intros a H0; case (decideGround a); simpl in |- *; try (intros; discriminate);
auto.
intros a b H0; case (decideGround a); simpl in |- *;
try (intros; discriminate); auto.
intros H1 H2; case (decideGround b); simpl in |- *;
try (intros; discriminate); auto.
intros H3 (H4, H5); case H3; auto.
intros H1 H2; case (decideGround b); simpl in |- *;
try (intros; discriminate); auto.
intros H3 (H4, H5); case H1; auto.
intros H3 (H4, H5); case H3; auto.
intros a b H0; case (decideGround a); simpl in |- *;
try (intros; discriminate); auto.
intros H1 H2; case (decideGround b); simpl in |- *;
try (intros; discriminate); auto.
intros H3 [H4| H4]; [ case H1 | case H3 ]; auto.
intros a b H0; case (decideGround a); simpl in |- *;
try (intros; discriminate); auto.
intros H1 H2; case (decideGround b); simpl in |- *;
try (intros; discriminate); auto.
intros H1 H2; case (decideGround b); simpl in |- *;
try (intros; discriminate); auto.
intros H3 H4; case H1; auto.
intros a b Ha Hb; generalize (Z_eq_bool_correct (exp2Z nil a) (exp2Z nil b));
case (Z_eq_bool (exp2Z nil a) (exp2Z nil b)); auto.
intros i a b Ha Hb; case (congZ_dec i (exp2Z nil a) (exp2Z nil b)); auto.
Qed.

shift deBrujn indices for expressions
• Variables under th are lifted of i
• Variables over th are lifted of o
Fixpoint shiftExp (th i o : nat) (a : exp) {struct a} : exp :=
match a with
| Plus b cPlus (shiftExp th i o b) (shiftExp th i o c)
| Num nNum n
| Var n
match ltdec n th with
| trueVar (n + i)
| falseVar (n + o)
end
end.

shift deBrujn indices for formulae
• Variables under th are lifted of i
• Variables over th are lifted of o
Fixpoint shiftForm (th i o : nat) (a : form) {struct a} : form :=
match a with
| Forall bForall b
| Exists bExists b
| ANd b cANd (shiftForm th i o b) (shiftForm th i o c)
| Or b cOr (shiftForm th i o b) (shiftForm th i o c)
| Imp b cImp (shiftForm th i o b) (shiftForm th i o c)
| Neg bNeg (shiftForm th i o b)
| TRueTRue
| FAlseFAlse
| Form.Eq b cForm.Eq (shiftExp th i o b) (shiftExp th i o c)
| Cong i1 b cCong i1 (shiftExp th i o b) (shiftExp th i o c)
end.

A formula with noBinder
Inductive noBinder : formProp :=
| nBTrue : noBinder TRue
| nBFalse : noBinder FAlse
| nBNeg : a : form, noBinder anoBinder (Neg a)
| nBAnd : a b : form, noBinder anoBinder bnoBinder (ANd a b)
| nBOr : a b : form, noBinder anoBinder bnoBinder (Or a b)
| nBImp : a b : form, noBinder anoBinder bnoBinder (Imp a b)
| nBEq : a b : exp, noBinder (Form.Eq a b)
| nBCong : (i : nat) (a b : exp), noBinder (Cong i a b).
Hint Constructors noBinder.

A list of pairs of integer and equations
Inductive listEqP : list (nat × form) → Prop :=
| listEqPnil : listEqP nil
| listEqPcons :
n a b l, 0 < nlistEqP llistEqP ((n, Form.Eq a b) :: l).

A list of pairs of integer and inequations
Inductive listNEqP : list (nat × form) → Prop :=
| listNEqPnil : listNEqP nil
| listNEqPcons :
n a b l,
0 < nlistNEqP llistNEqP ((n, Neg (Form.Eq a b)) :: l).

A list of pairs of integer and congruence
Inductive listCongP : list (nat × form) → Prop :=
| listCongPnil : listCongP nil
| listCongPcons :
n i a b l,
0 < i → 0 < nlistCongP llistCongP ((n, Cong i a b) :: l).

Hint Constructors listEqP.
Hint Constructors listCongP.
Hint Constructors listNEqP.

Some properties of lists
Theorem listEq_app :
l1 l2, listEqP l1listEqP l2listEqP (l1 ++ l2).
intros l1 l2 H1 H2; elim H1; simpl in |- *; auto.
Qed.

Theorem listNeq_app :
l1 l2, listNEqP l1listNEqP l2listNEqP (l1 ++ l2).
intros l1 l2 H1 H2; elim H1; simpl in |- *; auto.
Qed.

Theorem listCong_app :
l1 l2, listCongP l1listCongP l2listCongP (l1 ++ l2).
intros l1 l2 H1 H2; elim H1; simpl in |- *; auto.
Qed.
Hint Resolve listEq_app listNeq_app listCong_app.