The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Hello,
 Below is the same thing as Pierre's but using Prop, giving a proof of 
the axiom.
---Carlos


(** * Boolean algebra

 Coq formalization by Edsko de Vries, based on the second chapter
 (``The self-dual system of axioms'') in Goodstein's book ``Boolean 
Algebra''.
*)

Module BooleanAlgebra.

(** ** Term in a boolean algebra *)

Inductive trm : Set :=
 | true : trm
 | false : trm
 | or : trm -> trm -> trm
 | and : trm -> trm -> trm
 | not : trm -> trm.

(** ** Huntington's postulates *)

Inductive equiv : trm -> trm -> Prop :=
(** Commutativity *)
 | comm_or : forall (a b:trm), equiv (or a b) (or b a)
 | comm_and : forall (a b:trm), equiv (and a b) (and b a)
(** Distributivity *)
 | distr_or : forall (a b c:trm), equiv (or a (and b c)) (and (or a b) 
(or a c))
 | distr_and : forall (a b c:trm), equiv (and a (or b c)) (or (and a b) 
(and a c))
(** Identities *)
 | id_or : forall (a:trm), equiv (or a false) a
 | id_and : forall (a:trm), equiv (and a true) a
(** Complements *)
 | compl_or : forall (a:trm), equiv (or a (not a)) true
 | compl_and : forall (a:trm), equiv (and a (not a)) false
(** Closure *)
 | clos_not : forall (a b:trm), equiv a b -> equiv (not a) (not b)
 | clos_or : forall (a b c:trm), equiv a b -> equiv (or a c) (or b c)
 | clos_and : forall (a b c:trm), equiv a b -> equiv (and a c) (and b c)
(** Structural rules *)
 | refl : forall (a:trm), equiv a a
 | sym : forall (a b:trm), equiv a b -> equiv b a 
 | trans : forall (a b c:trm), equiv a b -> equiv b c -> equiv a c.


Definition trm_Prop : trm -> Prop.
intro.
induction H.
exact True. exact False.
exact ( IHtrm1 \/ IHtrm2).
exact (IHtrm1 /\ IHtrm2).
exact (~IHtrm).
Defined.

Lemma tpor : forall a b, trm_Prop (or a b) = (trm_Prop a \/ trm_Prop b).
intros.
trivial.
Qed.

Lemma tpnot : forall a, trm_Prop (not a) = ~(trm_Prop a).
intros.
trivial.
Qed.

Lemma tpand : forall a b, trm_Prop (and a b) = (trm_Prop a /\ trm_Prop b).
intros.
trivial.
Qed. 

Lemma tptrue : trm_Prop true = True.
trivial. Qed.

Lemma tpfalse : trm_Prop false = False.
trivial. Qed.

Definition decidab (P:Prop):= P \/ ~P.

Lemma decidab_or : forall P Q, decidab P -> decidab Q -> decidab (P\/Q).
Proof.
unfold decidab.
intuition.
Qed.

Lemma decidab_and : forall P Q, decidab P -> decidab Q -> decidab (P/\Q).
Proof.
unfold decidab.
intuition.
Qed.

Lemma decidab_not : forall P, decidab P -> decidab (~P).
Proof.
unfold decidab.
intuition.
Qed.

Lemma decidab_true : decidab True.
 Proof.
unfold decidab.
intuition.
Qed.

Lemma decidab_false : decidab False.
 Proof.
unfold decidab.
intuition.
Qed.



Lemma tpdec : forall a, decidab (trm_Prop a).
Proof.
intros.
induction a.
rewrite tptrue. apply decidab_true.
rewrite tpfalse. apply decidab_false.
rewrite tpor. apply decidab_or; assumption.
rewrite tpand. apply decidab_and; assumption.
rewrite tpnot. apply decidab_not; assumption.
Qed.



Lemma equiv_equiv : forall a b : trm, equiv a b ->
((trm_Prop a -> trm_Prop b)/\ (trm_Prop b -> trm_Prop a)).
Proof.
intros.
induction H.
apply conj.
rewrite tpor. rewrite tpor. 
intros.
induction H. apply or_intror. assumption.
apply or_introl. assumption.
rewrite tpor. rewrite tpor. 
intros.
induction H. apply or_intror. assumption.
apply or_introl. assumption.

apply conj; rewrite tpand; rewrite tpand; intros; induction H;
apply conj; assumption.

apply conj.
rewrite tpor; rewrite tpand; rewrite tpand; rewrite tpor; rewrite tpor.
intuition.
rewrite tpand; rewrite tpor; rewrite tpor; rewrite tpor; rewrite tpand.
intuition.

apply conj.
rewrite tpand. rewrite tpor. rewrite tpor.
rewrite tpand. rewrite tpand. intuition.
rewrite tpor. rewrite tpand. rewrite tpand.
rewrite tpand. intuition.

rewrite tpor. intuition.
rewrite tpor. intuition.

apply conj. rewrite tpor. rewrite tpfalse.
intuition.
rewrite tpor. intuition.

apply conj. rewrite tpand. intuition.
rewrite tpand. rewrite tptrue. intuition.

apply conj. rewrite tpor. rewrite tpnot.
rewrite tptrue. intuition.
rewrite tpor. rewrite tpnot.
assert (decidab (trm_Prop a)).
apply tpdec.
unfold decidab in H. intuition.

apply conj.
rewrite tpand. rewrite tpnot. rewrite tpfalse.
intuition.
rewrite tpfalse. intuition.


apply conj.
induction IHequiv.
rewrite tpnot. rewrite tpnot.
intros. intuition.

rewrite tpnot. rewrite tpnot. intuition.

apply conj.
rewrite tpor. rewrite tpor. intuition.
rewrite tpor. rewrite tpor. intuition.

apply conj. rewrite tpand. rewrite tpand.
intuition.
rewrite tpand. rewrite tpand. intuition.

apply conj.
intuition. intuition.
intuition.
intuition.
Qed.

Lemma true_false_distinct: ~equiv true false.
Proof.
intuition.
assert ((True -> False)/\ (False -> True)).
rewrite <- tptrue. rewrite <- tpfalse.
apply equiv_equiv. assumption.
induction H0. intuition.
Qed.




End BooleanAlgebra.