Library Presburger.Form


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
  • Addition
Inductive exp : Set :=
  | Num : nat → exp
  | Var : nat → exp
  | Plus : exp → exp → exp.

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

Define n.e as e+(n-1).e
Fixpoint scal (n : nat) : exp → exp :=
  fun e ⇒
  match n with
  | O ⇒ Num 0
  | S O ⇒ e
  | S n ⇒ Plus 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 n ⇒ Z_of_nat n
  | Var n ⇒ nth 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 c ⇒ form2Prop l b ∧ form2Prop l c
  | Or b c ⇒ form2Prop l b ∨ form2Prop l c
  | Imp b c ⇒ form2Prop l b → form2Prop l c
  | Neg b ⇒ ¬ form2Prop l b
  | TRue ⇒ True
  | FAlse ⇒ False
  | Form.Eq b c ⇒ exp2Z l b = exp2Z l c
  | Cong i b c ⇒ congZ 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
  | nil ⇒ TRue
  | e :: nil ⇒ e
  | e :: l1 ⇒ ANd 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
  | nil ⇒ True
  | _ ⇒ 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 : exp → Prop :=
  | GNum : ∀ i : nat, groundExp (Num i)
  | GPlus :
      ∀ a b : exp, groundExp a → groundExp b → groundExp (Plus a b).

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

A ground expression can be evaluated in an empty context
Theorem exp2Z_ground :
 ∀ (l : list Z) (e : exp), groundExp e → exp2Z 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 b ⇒ false
  | Exists b ⇒ false
  | ANd b c ⇒ decideGround b && decideGround c
  | Or b c ⇒ decideGround b || decideGround c
  | Imp b c ⇒ implb (decideGround b) (decideGround c)
  | Neg b ⇒ negb (decideGround b)
  | TRue ⇒ true
  | FAlse ⇒ false
  | Form.Eq b c ⇒ Z_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
 | true ⇒ form2Prop 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 c ⇒ Plus (shiftExp th i o b) (shiftExp th i o c)
  | Num n ⇒ Num n
  | Var n ⇒
      match ltdec n th with
      | true ⇒ Var (n + i)
      | false ⇒ Var (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 b ⇒ Forall b
  | Exists b ⇒ Exists b
  | ANd b c ⇒ ANd (shiftForm th i o b) (shiftForm th i o c)
  | Or b c ⇒ Or (shiftForm th i o b) (shiftForm th i o c)
  | Imp b c ⇒ Imp (shiftForm th i o b) (shiftForm th i o c)
  | Neg b ⇒ Neg (shiftForm th i o b)
  | TRue ⇒ TRue
  | FAlse ⇒ FAlse
  | Form.Eq b c ⇒ Form.Eq (shiftExp th i o b) (shiftExp th i o c)
  | Cong i1 b c ⇒ Cong i1 (shiftExp th i o b) (shiftExp th i o c)
  end.

A formula with noBinder
Inductive noBinder : form → Prop :=
  | nBTrue : noBinder TRue
  | nBFalse : noBinder FAlse
  | nBNeg : ∀ a : form, noBinder a → noBinder (Neg a)
  | nBAnd : ∀ a b : form, noBinder a → noBinder b → noBinder (ANd a b)
  | nBOr : ∀ a b : form, noBinder a → noBinder b → noBinder (Or a b)
  | nBImp : ∀ a b : form, noBinder a → noBinder b → noBinder (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 < n → listEqP l → listEqP ((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 < n → listNEqP l → listNEqP ((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 < n → listCongP l → listCongP ((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 l1 → listEqP l2 → listEqP (l1 ++ l2).
intros l1 l2 H1 H2; elim H1; simpl in |- *; auto.
Qed.

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

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