famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[coq] commutative semi ring

This commit is contained in:
Julin S 2023-10-12 13:07:43 +05:30
parent c49c2c3d96
commit 4f3524269f
1 changed files with 214 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

214
coq/bool3csr.v Normal file
View File

@ -0,0 +1,214 @@
(* 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.