[coq] [mathcomp] make ssreflect version of bool3
This commit is contained in:
parent
4f3524269f
commit
8cb107c63c
|
|
@ -0,0 +1,240 @@
|
|||
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.
|
||||
|
|
@ -1,3 +1,15 @@
|
|||
Print ex.
|
||||
Print sig.
|
||||
Print proj2.
|
||||
Print proj1.
|
||||
Check proj1_sig.
|
||||
Check proj2_sig.
|
||||
Print sigT.
|
||||
Search projT2.
|
||||
Check projT2.
|
||||
Print sumor.
|
||||
Locate "exists".
|
||||
|
||||
Module Interval.
|
||||
Definition t (low high: nat): Type :=
|
||||
{x:nat | (x >= low) /\ (x <= high)}.
|
||||
|
|
@ -64,6 +76,12 @@ From mathcomp Require Import all_ssreflect all_algebra.
|
|||
(* From mathcomp Require Import algebra.matrix. *)
|
||||
(* Check matrix. *)
|
||||
|
||||
Check bool.
|
||||
Print RingType.
|
||||
Print ringType.
|
||||
Print GRing.Ring.type.
|
||||
Print GRing.Ring.class_of.
|
||||
|
||||
Local Open Scope type_scope.
|
||||
Local Open Scope ring_scope.
|
||||
|
||||
|
|
@ -96,7 +114,7 @@ Fail Check \matrix_(i<3, j<7) if (i:nat)==j then 1 else 0.
|
|||
Fail Check \matrix_(i<3, j<7) (fun i:'I_3 j => if i==j then 1 else 0).
|
||||
Check 1%:M.
|
||||
|
||||
Definition M3 : 'M[int]_(2,2) := \matrix_(i,j < 2) 3%:Z.
|
||||
Definition M2 : 'M[int]_(2,2) := \matrix_(i,j < 2) 3%:Z.
|
||||
Example eg1: 'M[int]_ (3, 7) := \matrix_(i<3, j<7) 8%:Z.
|
||||
Example eg2: 'M[int]_ (3, 7) := \matrix_(i<3, j<7) 8.
|
||||
Check 3%:Z.
|
||||
|
|
@ -105,9 +123,64 @@ Print Scopes.
|
|||
Example eg3 := \matrix_(i<3, j<7)
|
||||
(fun i j => if i==j :> nat then 1 else 0%:Z).
|
||||
|
||||
Example eg4 := \matrix_(i<3, j<3)
|
||||
(fun i j => i+j%:Z).
|
||||
Compute eg4 0 1.
|
||||
|
||||
Example eg4 := \matrix_(i<3, j<3) (i+j).
|
||||
(* Example eg4 := \matrix_(i<3, j<3) *)
|
||||
(* (fun i j => i+j%:Z). *)
|
||||
(* Compute eg4 0 1. *)
|
||||
Check mxE tt eg4.
|
||||
|
||||
Locate "=2".
|
||||
|
||||
Example eg5 := \matrix_(i<3, j<3) (Some (Nat.eqb i j)).
|
||||
Check map_mx (fun x =>
|
||||
match x with
|
||||
| Some true => None
|
||||
| _ => x
|
||||
end).
|
||||
Definition eg5' := map_mx (fun x =>
|
||||
match x with
|
||||
| Some true => None
|
||||
| _ => x
|
||||
end) eg5.
|
||||
|
||||
|
||||
Goal eg5 0 1 = Some false.
|
||||
rewrite /eg5 !mxE /=. Abort.
|
||||
Goal eg5' 1 1 = None.
|
||||
rewrite /eg5' !mxE /=. Abort.
|
||||
|
||||
Print ordinal.
|
||||
Check Ordinal (m:=3).
|
||||
Fail Check Ordinal (_:3<5).
|
||||
|
||||
(* Has to be at least one row and one column *)
|
||||
Definition matLinker {rows cols: nat}
|
||||
(mat: 'M[option bool]_(rows.+1, cols.+1))
|
||||
: 'M[option bool]_(rows.+1, cols.+1).
|
||||
Proof.
|
||||
refine (
|
||||
let colid := Ordinal (m:=cols) (n:=cols.+1) _ in
|
||||
let mapfn :=
|
||||
fun ob => match ob with
|
||||
| Some true => None
|
||||
| _ => ob
|
||||
end in
|
||||
let lastcol := col colid mat in
|
||||
let lastcol' := map_mx mapfn lastcol in
|
||||
let mat' := col' colid mat in
|
||||
let res := row_mx mat' lastcol' in _).
|
||||
move: mat' res.
|
||||
rewrite PeanoNat.Nat.pred_succ.
|
||||
by rewrite addn1.
|
||||
Unshelve.
|
||||
by [].
|
||||
Show Proof.
|
||||
Defined.
|
||||
|
||||
Check matLinker eg5.
|
||||
|
||||
|
||||
Check eg4.
|
||||
Fail Check eg4 _ 0 _ 0.
|
||||
Compute eg4 0 0.
|
||||
|
|
@ -115,6 +188,8 @@ Check eg4 0 0.
|
|||
Search (int_ZmodType -> nat -> int_ZmodType).
|
||||
Check eg2 _ _.
|
||||
Check eg4 _ _.
|
||||
Check eg4 0 0.
|
||||
Compute eg4 0 0.
|
||||
|
||||
Check matrix bool 3 4.
|
||||
(* 'M_(3, 4) : predArgType *)
|
||||
|
|
@ -132,6 +207,11 @@ Check 'M[bool]_(3, 4).
|
|||
Fail Check MatrixFormula.seq_of_rV eg4.
|
||||
From CoqEAL Require Import hrel param refinements trivial_seq seqmx.
|
||||
|
||||
Check eg2.
|
||||
Compute (addmx eg2 eg2) 1 1.
|
||||
Check 1%:M.
|
||||
Check 0%:M.
|
||||
Check M.
|
||||
|
||||
Check mkseqmx_ord.
|
||||
Check matrix_of_fun.
|
||||
|
|
@ -174,18 +254,18 @@ Restart.
|
|||
by rewrite size_map.
|
||||
Qed.
|
||||
|
||||
Goal forall n:nat,
|
||||
size (ord_enum n) = n.
|
||||
Proof.
|
||||
move=> n.
|
||||
Search size.
|
||||
rewrite -{3}(size_iota 0 n).
|
||||
Search ord_enum.
|
||||
rewrite -val_ord_enum.
|
||||
Search size.
|
||||
by rewrite size_map.
|
||||
Search ord_enum.
|
||||
Qed.
|
||||
(* Goal forall n:nat, *)
|
||||
(* size (ord_enum n) = n. *)
|
||||
(* Proof. *)
|
||||
(* move=> n. *)
|
||||
(* Search size. *)
|
||||
(* rewrite -{3}(size_iota 0 n). *)
|
||||
(* Search ord_enum. *)
|
||||
(* rewrite -val_ord_enum. *)
|
||||
(* Search size. *)
|
||||
(* by rewrite size_map. *)
|
||||
(* Search ord_enum. *)
|
||||
(* Qed. *)
|
||||
|
||||
Definition mkRow {A:Type} {rows cols:nat}
|
||||
(r: 'I_rows) (f: 'I_rows -> 'I_cols -> A): Vector.t A cols.
|
||||
|
|
@ -193,17 +273,13 @@ refine(
|
|||
match r with
|
||||
| @Ordinal _ r' _ =>
|
||||
let cids := Vector.of_list (ord_enum cols) in (* list 'I_cols *)
|
||||
let mapped := Vector.map (fun cid => f r cid) cids in
|
||||
let rw := Vector.map (fun cid => f r cid) cids in
|
||||
_
|
||||
end).
|
||||
assert ((size (ord_enum cols)) = cols).
|
||||
by rewrite size_ord_enum.
|
||||
move: mapped.
|
||||
by rewrite (length_size (ord_enum cols)) H.
|
||||
move: rw.
|
||||
by rewrite length_size size_ord_enum.
|
||||
Defined.
|
||||
|
||||
Check Vector.fold_right.
|
||||
|
||||
Definition mkMat {A:Type} {rows cols:nat}
|
||||
(f: 'I_rows -> 'I_cols -> A): Vector.t (Vector.t A cols) rows.
|
||||
Proof.
|
||||
|
|
@ -213,16 +289,53 @@ Proof.
|
|||
(* let res := Vector.fold_right (fun rw acc => rw ++ acc) rws [] in *)
|
||||
_).
|
||||
move: rws.
|
||||
by rewrite (length_size (ord_enum rows)) (size_ord_enum).
|
||||
(* by rewrite (length_size (ord_enum rows)) (size_ord_enum). *)
|
||||
by rewrite length_size size_ord_enum.
|
||||
Defined.
|
||||
|
||||
Compute mkMat (fun_of_matrix eg4).
|
||||
Check (fun_of_matrix M2).
|
||||
Check (fun_of_matrix eg3).
|
||||
|
||||
Definition xm2 := mkMat (fun_of_matrix M2).
|
||||
Definition xm3 := mkMat (fun_of_matrix eg3).
|
||||
Definition xm4 := mkMat (fun_of_matrix eg4).
|
||||
Check 'M_(3,4).
|
||||
|
||||
|
||||
Definition mkseqmx_ord {A: Type} m n (f : 'I_m -> 'I_n -> A): nat.
|
||||
Abort.
|
||||
|
||||
Require Import Extraction.
|
||||
Extraction Language Haskell.
|
||||
Require Import ExtrHaskellBasic.
|
||||
Require Import ExtrHaskellZInteger.
|
||||
Require Import ExtrHaskellNatNum.
|
||||
|
||||
Check 0xff.
|
||||
Definition nnnn: nat := 0xf.
|
||||
Check 'rV[bool]_nnnn.
|
||||
Check 'M_(0, 0).
|
||||
|
||||
|
||||
Definition M0: 'M_0 :=
|
||||
\matrix_(i<0, j<0) false.
|
||||
|
||||
Definition R0 (cols: nat) :=
|
||||
\matrix_(i<0, j<cols) false.
|
||||
Check R0 3.
|
||||
Check \matrix_(i<1, j<0) true.
|
||||
About bool.
|
||||
About int.
|
||||
|
||||
Definition C0 (rows: nat): 'cV_0 :=
|
||||
\matrix_(i<0, j<cols) false.
|
||||
\matrix_(i<0, j<0) (fun i j => if i==j :> nat then true else false).
|
||||
|
||||
(* Extract Inductive "Vector.t _ n" => "Vec" [ "Nil" "(:>)" ]. *)
|
||||
Extract Inductive Vector.t => "Vec" [ "Nil" "(:>)" ].
|
||||
Recursive Extraction xm2.
|
||||
Recursive Extraction eg3.
|
||||
|
||||
Example e1 := (ord_enum 2).
|
||||
Recursive Extraction e1. (* Ocaml ran this! *)
|
||||
Recursive Extraction smx4. (* Ocaml couldn't run this.. *)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,53 @@
|
|||
(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment1.ipynb *)
|
||||
|
||||
(* cond_dup: 'a list -> ('a -> bool) -> 'a list *)
|
||||
let cond_dup l f =
|
||||
List.fold_right
|
||||
(fun a acc ->
|
||||
(if f a then a :: a :: acc
|
||||
else a :: acc))
|
||||
l []
|
||||
(* # cond_dup [3;4;5] (fun x -> x mod 2 = 1);; *)
|
||||
(* - : int list = [3; 3; 4; 5; 5] *)
|
||||
|
||||
let rec n_times (f, n, v) =
|
||||
if n <= 0 then v
|
||||
else n_times (f, n-1, f v)
|
||||
(* # n_times((fun x-> x+1), 50, 0);; *)
|
||||
(* - : int = 50 *)
|
||||
|
||||
let rec range start stop =
|
||||
if stop - start >= 0 then start :: (range (start+1) stop)
|
||||
else []
|
||||
(* # range 2 5;; *)
|
||||
(* - : int list = [2; 3; 4; 5] *)
|
||||
|
||||
let rec zipwith f a b =
|
||||
match a, b with
|
||||
| [], _
|
||||
| _, [] -> []
|
||||
| a'::aa, b'::bb -> (f a' b') :: (zipWith f aa bb)
|
||||
(* # zipwith (+) [1;2;3] [4;5];; *)
|
||||
(* - : int list = [5; 7] *)
|
||||
|
||||
(* let rec flatten l = *)
|
||||
(* match l with *)
|
||||
(* | [] -> [] *)
|
||||
(* | l :: ls -> l @ (flatten ls) *)
|
||||
let rec flatten = function
|
||||
| [] -> []
|
||||
| l :: ls -> l @ (flatten ls)
|
||||
(* # flatten ([[1;2];[3;4]]);; *)
|
||||
(* - : int list = [1; 2; 3; 4] *)
|
||||
|
||||
let remove_stutter l =
|
||||
List.fold_right
|
||||
(fun x (prev, res) ->
|
||||
match prev with
|
||||
| None -> (Some x, x::res)
|
||||
| Some prev' ->
|
||||
if x=prev' then (prev, res)
|
||||
else (Some x, x::res))
|
||||
l (None, [])
|
||||
(* # remove_stutter [1;2;2;3;1;1;1;4;4;2;2];; *)
|
||||
(* - : int option * int list = (Some 1, [1; 2; 3; 1; 4; 2]) *)
|
||||
Loading…
Reference in New Issue