241 lines
5.0 KiB
Coq
241 lines
5.0 KiB
Coq
Require Import ssreflect.
|
|
|
|
(* Commutative semi ring *)
|
|
|
|
Module Type CSR.
|
|
Parameter R: Type.
|
|
Parameter zero: R.
|
|
Parameter one: R.
|
|
Parameter add: R -> R -> R.
|
|
Parameter mul: R -> R -> R.
|
|
|
|
Parameter addZero: forall a:R,
|
|
add zero a = a.
|
|
Parameter mulOne: forall a:R,
|
|
mul one a = a.
|
|
Parameter mulZero: forall a:R,
|
|
mul zero a = zero.
|
|
|
|
Parameter addC: forall a b:R,
|
|
add a b = add b a.
|
|
Parameter mulC: forall a b:R,
|
|
mul a b = mul b a.
|
|
|
|
Parameter addA: forall a b c:R,
|
|
add a (add b c) = add (add a b) c.
|
|
Parameter mulA: forall a b c:R,
|
|
mul a (mul b c) = mul (mul a b) c.
|
|
|
|
Parameter mulAddDistr: forall a b c:R,
|
|
mul a (add b c) = add (mul a b) (mul a c).
|
|
End CSR.
|
|
|
|
Module B2 <: CSR.
|
|
Definition R := bool.
|
|
Definition zero := false.
|
|
Definition one := true.
|
|
Definition add := xorb.
|
|
Definition mul := andb.
|
|
|
|
Lemma addZero: forall a:R,
|
|
add zero a = a.
|
|
Proof. move=> a; by case: a. Qed.
|
|
Lemma mulOne: forall a:R,
|
|
mul one a = a.
|
|
Proof. move=> a; by case: a. Qed.
|
|
|
|
Lemma mulZero: forall a:R,
|
|
mul zero a = zero.
|
|
Proof. move=> a; by case: a. Qed.
|
|
|
|
Lemma addC: forall a b:R,
|
|
add a b = add b a.
|
|
Proof. move=> a; by case: a. Qed.
|
|
|
|
Lemma mulC: forall a b:R,
|
|
mul a b = mul b a.
|
|
Proof. move=> a b; by case: a; case: b. Qed.
|
|
|
|
Lemma addA: forall a b c:R,
|
|
add a (add b c) = add (add a b) c.
|
|
Proof. move=> a b c; by case: a; case: b; case c. Qed.
|
|
|
|
Lemma mulA: forall a b c:R,
|
|
mul a (mul b c) = mul (mul a b) c.
|
|
Proof. move=> a b c; by case: a; case: b; case c. Qed.
|
|
|
|
Lemma mulAddDistr: forall a b c:R,
|
|
mul a (add b c) = add (mul a b) (mul a c).
|
|
Proof. move=> a b c; by case: a; case: b; case c. Qed.
|
|
End B2.
|
|
|
|
Module B3 <: CSR.
|
|
Definition R := option bool.
|
|
Definition zero := Some false.
|
|
Definition one := Some true.
|
|
|
|
Definition add (a b: R): R :=
|
|
match a, b with
|
|
| Some true, _ => Some true
|
|
| _, Some true => Some true
|
|
| Some false, Some false => Some false
|
|
| _, _ => None
|
|
end.
|
|
Definition mul (a b: R): R :=
|
|
match a, b with
|
|
| Some false, _ => Some false
|
|
| _, Some false => Some false
|
|
| Some true, Some true => Some true
|
|
| _, _ => None
|
|
end.
|
|
|
|
Lemma addZero: forall a:R,
|
|
add zero a = a.
|
|
Proof.
|
|
move=> a; case: a.
|
|
move=> a; by case: a.
|
|
by [].
|
|
Qed.
|
|
|
|
Lemma mulOne: forall a:R,
|
|
mul one a = a.
|
|
Proof.
|
|
move=> a; case: a.
|
|
move=> a; by case: a.
|
|
by [].
|
|
Qed.
|
|
|
|
Lemma mulZero: forall a:R,
|
|
mul zero a = zero.
|
|
Proof.
|
|
move=> a; case: a.
|
|
move=> a; by case: a.
|
|
by [].
|
|
Qed.
|
|
|
|
Lemma addC: forall a b:R,
|
|
add a b = add b a.
|
|
Proof.
|
|
move=> a b.
|
|
case: a.
|
|
move=> a.
|
|
case: a.
|
|
case: b.
|
|
move=> a.
|
|
case: a.
|
|
all: by [].
|
|
Qed.
|
|
|
|
Lemma mulC: forall a b:R,
|
|
mul a b = mul b a.
|
|
Proof.
|
|
move=> a b.
|
|
case: a.
|
|
move=> a.
|
|
case: a.
|
|
case: b.
|
|
move=> a.
|
|
case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: b.
|
|
move=> a.
|
|
case: a.
|
|
all: by [].
|
|
Qed.
|
|
|
|
(* Quite sure this could be way better than this *)
|
|
Lemma addA: forall a b c:R,
|
|
add a (add b c) = add (add a b) c.
|
|
Proof.
|
|
move=> a b c; case: a.
|
|
move=> a; case: a.
|
|
case: b.
|
|
move=>a; case: a.
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: b.
|
|
move=>a; case: a.
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: b.
|
|
move=>a; case: a.
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
case: c.
|
|
move=>a; case: a.
|
|
by [].
|
|
by [].
|
|
by [].
|
|
Qed.
|
|
|
|
Lemma mulA: forall a b c:R,
|
|
mul a (mul b c) = mul (mul a b) c.
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- induction b as [b|].
|
|
+ induction c as [c|].
|
|
* induction a; induction b; induction c; now simpl.
|
|
* induction a; induction b; now simpl.
|
|
+ induction c as [c|].
|
|
* induction a; induction c; now simpl.
|
|
* induction a; now simpl.
|
|
- induction b as [b|].
|
|
+ induction c as [c|].
|
|
* induction b; induction c; now simpl.
|
|
* induction b; now simpl.
|
|
+ induction c.
|
|
* induction a; now simpl.
|
|
* now simpl.
|
|
Qed.
|
|
|
|
Lemma mulAddDistr: forall a b c:R,
|
|
mul a (add b c) = add (mul a b) (mul a c).
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- induction b as [b|].
|
|
+ induction c as [c|].
|
|
* induction a; induction b; induction c; now simpl.
|
|
* induction a; induction b; now simpl.
|
|
+ induction c as [c|].
|
|
* induction a; induction c; now simpl.
|
|
* induction a; now simpl.
|
|
- induction b as [b|].
|
|
+ induction c as [c|].
|
|
* induction b; induction c; now simpl.
|
|
* induction b; now simpl.
|
|
+ induction c.
|
|
* induction a; now simpl.
|
|
* now simpl.
|
|
Qed.
|
|
End B3.
|