215 lines
5.2 KiB
Coq
215 lines
5.2 KiB
Coq
(* 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. induction a; intuition. Qed.
|
|
Lemma mulOne: forall a:R,
|
|
mul one a = a.
|
|
Proof. induction a; intuition. Qed.
|
|
|
|
Lemma mulZero: forall a:R,
|
|
mul zero a = zero.
|
|
Proof. induction a; intuition. Qed.
|
|
|
|
Lemma addC: forall a b:R,
|
|
add a b = add b a.
|
|
Proof. induction a; intuition. Qed.
|
|
|
|
Lemma mulC: forall a b:R,
|
|
mul a b = mul b a.
|
|
Proof. induction a; induction b; intuition. Qed.
|
|
|
|
Lemma addA: forall a b c:R,
|
|
add a (add b c) = add (add a b) c.
|
|
Proof. induction a; induction b; induction c; intuition. Qed.
|
|
|
|
Lemma mulA: forall a b c:R,
|
|
mul a (mul b c) = mul (mul a b) c.
|
|
Proof. induction a; induction b; induction c; intuition. Qed.
|
|
|
|
Lemma mulAddDistr: forall a b c:R,
|
|
mul a (add b c) = add (mul a b) (mul a c).
|
|
Proof. induction a; induction b; induction c; intuition. Qed.
|
|
End B2.
|
|
|
|
Module B3 <: CSR.
|
|
Definition R := option bool.
|
|
Definition zero := Some false.
|
|
Definition one := Some true.
|
|
|
|
(* Definition lift (f: bool -> bool -> bool): *)
|
|
(* option bool -> option bool -> option bool := *)
|
|
(* fun a b => *)
|
|
(* match a, b with *)
|
|
(* | Some a, Some b => Some (f a b) *)
|
|
(* | _, _ => None *)
|
|
(* end. *)
|
|
(* Definition add := lift xorb. *)
|
|
|
|
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.
|
|
intro a.
|
|
induction a.
|
|
- induction a; intuition.
|
|
- unfold zero; trivial.
|
|
Qed.
|
|
|
|
Lemma mulOne: forall a:R,
|
|
mul one a = a.
|
|
Proof.
|
|
intro a.
|
|
induction a.
|
|
- induction a; intuition.
|
|
- unfold zero; trivial.
|
|
Qed.
|
|
|
|
Lemma mulZero: forall a:R,
|
|
mul zero a = zero.
|
|
Proof.
|
|
intro a.
|
|
induction a.
|
|
- induction a; intuition.
|
|
- unfold zero; trivial.
|
|
Qed.
|
|
|
|
Lemma addC: forall a b:R,
|
|
add a b = add b a.
|
|
Proof.
|
|
intro a.
|
|
induction a.
|
|
- induction a; induction b; simpl.
|
|
+ now induction a.
|
|
+ trivial.
|
|
+ now induction a.
|
|
+ trivial.
|
|
- intro b; now induction b.
|
|
Qed.
|
|
|
|
Lemma mulC: forall a b:R,
|
|
mul a b = mul b a.
|
|
Proof.
|
|
intro a.
|
|
induction a.
|
|
- induction a; induction b; simpl.
|
|
+ now induction a.
|
|
+ trivial.
|
|
+ now induction a.
|
|
+ trivial.
|
|
- intro b; now induction b.
|
|
Qed.
|
|
|
|
Lemma addA: forall a b c:R,
|
|
add a (add b c) = add (add 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 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.
|