From 5897e8d04b79f6959d657b99353403faa67a4ffa Mon Sep 17 00:00:00 2001 From: Julin S Date: Sat, 28 Oct 2023 23:38:24 +0530 Subject: [PATCH] add some older files --- coq/mathcomp/bigop-egs.v | 7 ++ coq/mathcomp/general.v | 12 ++- coq/mathcomp/matrix-egs.v | 3 + coq/mathcomp/matrix.v | 47 +++++++++++ coq/matrix.v | 35 ++++++-- ocaml/ex1.ml | 173 +++++++++++++++++++++++++++++++++++++- 6 files changed, 261 insertions(+), 16 deletions(-) diff --git a/coq/mathcomp/bigop-egs.v b/coq/mathcomp/bigop-egs.v index f41689d..4e1a289 100644 --- a/coq/mathcomp/bigop-egs.v +++ b/coq/mathcomp/bigop-egs.v @@ -3,3 +3,10 @@ From mathcomp Require Import all_ssreflect all_algebra. Lemma sum_odd_3: \sum_(0 <= i < 3.*2 | odd i) i = 3^2. Proof. by rewrite unlock /=. Qed. + +Lemma sum_nat_const_I3 n : \sum_(i in 'I_3) n = #|'I_3| * n. +Proof. + rewrite big_const. + rewrite iter_addn_0. + by rewrite mulnC. +Qed. diff --git a/coq/mathcomp/general.v b/coq/mathcomp/general.v index 5846ee5..3fc277d 100644 --- a/coq/mathcomp/general.v +++ b/coq/mathcomp/general.v @@ -1,10 +1,14 @@ From mathcomp Require Import all_ssreflect. (** * Using [exists] *) +(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/exists.20with.20ssreflect *) Goal forall w:seq nat, - (exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::]. + (exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::]. Proof. - move=> w [w1 [w2]]. - by case; case: w; case: w1; case: w2. + move=> w [w1 [w2]]. + by case; case: w; case: w1; case: w2. (* ✓ *) +Restart. + move=> w [w1 [w2]] [_]. + rewrite size_eq0. + by apply/eqP. Qed. - diff --git a/coq/mathcomp/matrix-egs.v b/coq/mathcomp/matrix-egs.v index c6e48ad..c45254d 100644 --- a/coq/mathcomp/matrix-egs.v +++ b/coq/mathcomp/matrix-egs.v @@ -22,3 +22,6 @@ Proof. rewrite /fun_of_matrix /=. by rewrite ffunE. Qed. + +Check castmx. +Print erefl. diff --git a/coq/mathcomp/matrix.v b/coq/mathcomp/matrix.v index 58ea86f..cb1ad14 100644 --- a/coq/mathcomp/matrix.v +++ b/coq/mathcomp/matrix.v @@ -113,6 +113,7 @@ Check \matrix_(i<3, j<7) if (i==j:>nat) then 1%:Z else 0. 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. +Check const_mx (Some false): 'M_3. 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. @@ -122,6 +123,32 @@ Print Scope Z_scope. Print Scopes. Example eg3 := \matrix_(i<3, j<7) (fun i j => if i==j :> nat then 1 else 0%:Z). +Locate "&&". +Example eg6 := \matrix_(i<3, j<7) + (if (i==0) && (j==1) then (Some true) else (Some false)). +(* Example eg6 := \matrix_(i<3, j<7) *) +(* (if (i==0) && (j==1) then 1 else 0%:Z). *) +(* Example eg6 := \matrix_(i<3, j<7) *) +(* (if ((i==0) && (j==1)) then 1 else 0%:Z). *) +(* Example eg6 := \matrix_(i<3, j<7) *) +(* (fun i j => if ((i=0:>nat) && (j=1):>nat) then 1 else 0%:Z). *) +(* Example eg6 := \matrix_(i<3, j<7) *) +(* (fun i j => if (i=0 && j=1):>nat then 1 else 0%:Z). *) + +Example eg7: 'rV_2 := + \row_(i<2) (if i==0 then true else false). +Check 1%:M: 'M_2. +Check eg7. + +Example eg8: 'cV_2 := + \col_(i<2) (if i!=0 then true else false). +Check eg7 *m eg8. + +Example eg7ob: 'rV_2 := + \row_(i<2) (if i==0 then Some true else Some false). +Example eg8ob: 'cV_2 := + \col_(i<2) (if i!=0 then Some true else Some false). + Example eg4 := \matrix_(i<3, j<3) (i+j). @@ -204,6 +231,26 @@ Check 'M[bool]_(3, 4). (* 'M_(3, 4) : predArgType *) +Local Open Scope ring_scope. + +Lemma sum_odd_n (n: nat) : \sum_(0 <= i < n.*2 | odd i) i = n^2. +Proof. + elim: n => [//=|n IH]; first by rewrite double0 -mulnn muln0 big_geq. +rewrite (@big_cat_nat _ _ _ n.*2) //=; last by rewrite -!addnn leq_add. +rewrite IH -!mulnn mulSnr mulnSr -addnA. +congr (_ + _). +rewrite big_ltn_cond ?ifF ?odd_double //. +rewrite big_ltn_cond /ifT ?oddS ?odd_double //=. +by rewrite big_geq ?addn0 -addnn addnS // -addnn addSn. +Qed. + + + + + + + + Fail Check MatrixFormula.seq_of_rV eg4. From CoqEAL Require Import hrel param refinements trivial_seq seqmx. diff --git a/coq/matrix.v b/coq/matrix.v index 7e79999..fbd5e09 100644 --- a/coq/matrix.v +++ b/coq/matrix.v @@ -5,8 +5,17 @@ Require Import Bvector. Definition matrix (rows cols: nat): Type := Vector.t (Bvector cols) rows. -Axiom zip: forall {A B: Type} {n:nat}, - Vector.t A n -> Vector.t B n -> Vector.t (A*B) n. +(* Uses /convoy pattern/. + +See: https://stackoverflow.com/questions/59290356/dependent-pattern-matching-zip-two-vectors + *) +Fixpoint zip {A B: Type} {n:nat} + (av: Vector.t A n) (bv: Vector.t B n): Vector.t (A*B) n := + match av in Vector.t _ n + return Vector.t B n -> Vector.t (A*B) n with + | [] => fun _ => [] + | a::av' => fun bv => (a, Vector.hd bv) :: zip av' (Vector.tl bv) + end bv. Section Matrix. Context {A: Type}. @@ -20,10 +29,20 @@ Section Matrix. Definition vecMatrixProd {rows cols: nat} (vec: Bvector rows) (mat: matrix cols rows): Bvector cols := Vector.map (fun mrow => dotProduct vec mrow) mat. - - - Definition vecMatrixProd {rows cols: nat} - (vec: Bvector rows) (mat: matrix cols rows): Bvector cols := - Vector.map (fun mrow => dotProduct vec mrow) mat. - End Matrix. + +Definition isAllZero {n:nat} (v: Vector.t bool n): bool := + negb (Vector.fold_right (fun elem acc => orb elem acc) v false). + + +(* Make vector of size [sz] with its [i]-th bit set, where indexing + starts from 0. *) +Fixpoint seti (i sz:nat): Vector.t bool sz := + match sz with + | O => [] + | S sz' => + match i with + | O => true :: (repeat false sz') + | S i' => false :: (seti i' sz') + end + end. diff --git a/ocaml/ex1.ml b/ocaml/ex1.ml index 6638679..0bbd652 100644 --- a/ocaml/ex1.ml +++ b/ocaml/ex1.ml @@ -40,14 +40,179 @@ let rec flatten = function (* # flatten ([[1;2];[3;4]]);; *) (* - : int list = [1; 2; 3; 4] *) -let remove_stutter l = - List.fold_right +let remove_stutter l = snd (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, []) + 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]) *) +(* - : int list = [1; 2; 3; 1; 4; 2] *) + + +(*********************************************************************) + + +(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment2.zip *) + +type expr + = Var of string + | App of expr * expr + | Lam of string * expr + +(* prettify: expr -> string *) +let rec prettify e = + match e with + | Var v -> v + | App (e1, e2) -> "(" ^ (prettify e1) ^ " " ^ (prettify e2) ^ ")" + | Lam (v, e') -> "λ" ^ v ^ "." ^ (prettify e') + +let mem v vars = List.exists (fun x -> x=v) vars + +(* # mem "b" ["a";"b";"c"];; *) +(* - : bool = true *) +(* *) +(* # mem "x" ["a";"b";"c"];; *) +(* - : bool = false *) + +let remove v vars = List.filter (fun x -> not (v=x)) vars + +(* # remove "b" ["a";"b";"c"];; *) +(* - : string list = ["a"; "c"] *) +(* *) +(* # remove "x" ["a";"b";"c"];; *) +(* - : string list = ["a"; "b"; "c"] *) + +(* union: string list -> string list -> string list *) +let union s1 s2 = + remove_stutter (List.sort String.compare (s1 @ s2)) + +(* # union ["a"; "c"; "b"] ["d"; "b"; "x"; "a"];; *) +(* - : String.t list = ["a"; "b"; "c"; "d"; "x"] *) + +let add a l = + let l' = + (if List.exists (fun x -> x=a) l then l + else a::l) in + List.sort + (fun x y -> + if x < y then -1 + else if x = y then 0 + else 1) l' + +(* # add "b" ["a";"c"];; *) +(* - : string list = ["a"; "b"; "c"] *) +(* *) +(* # add "a" ["c"; "a"];; *) +(* - : string list = ["a"; "c"] *) + +let varcount = ref 0 +let fresh s = + let v = !varcount in + s ^ (string_of_int v) + +(* free_variables: expr -> string list *) +let rec free_variables = function + | Var v -> [v] + | App (e1, e2) -> + let fv1 = free_variables e1 in + let fv2 = free_variables e2 in + union fv1 fv2 + | Lam (v, e') -> + let fv = free_variables e' in + remove v fv + +(* # free_variables (Lam ("x", Var "x"));; *) +(* - : String.t list = [] *) +(* *) +(* # free_variables (Lam ("x", Var "y"));; *) +(* - : String.t list = ["y"] *) + +(* substitute : expr -> string -> expr -> expr *) +(* substitute e1 var e2 means e1[e2/var] *) +let rec substitute e var repl = + match e with + | Var v -> repl + | App (e1, e2) -> App (substitute e1 var repl, substitute e2 var repl) + | Lam (v, body) -> + if v=var then + (* A bound variable. Can be interfered with only on a beta-reduction *) + e + else + let v' = + (* Avoid free variable capture *) + if mem v (free_variables repl) then fresh v + else v in + let body' = substitute body var repl in + Lam (v', body') + +(* (λy.x)[(λz.z w)/x] is (λy.λz.z w) *) +(* # substitute (Lam ("y", Var "x")) "x" (Lam ("z", App (Var "z", (Var "w"))));; *) +(* - : expr = Lam ("y", Lam ("z", App (Var "z", Var "w"))) *) +(* *) +(* (λx.x)[y/x] is (λx.x) *) +(* # substitute (Lam ("x", Var "x")) "x" (Var "y");; *) +(* - : expr = Lam ("x", Var "x") *) +(* *) +(* (λx.y)[x/y] is (λx0. x) *) +(* # substitute (Lam ("x", Var "y")) "y" (Var "x");; *) +(* - : expr = Lam ("x0", Var "x") *) + + +(* reduce_cbv : expr -> expr * bool *) +let reduce_cbv e = + match e with + | App (e1, e2) -> + (match e1 with + | Lam (v, e') -> (substitute e' v e2, true) + | _ -> + (* Still got space to reduce *) + let (e1', flag) = reduce_cbv e1 in + (App (e1', e2), flag)) + | _ -> (e, false) + +(* # let e, flag = *) +(* reduce_cbv ( *) +(* App ( *) +(* App ( *) +(* Lam ("x", Var "x"), *) +(* Lam ("x", Var "x")), *) +(* Lam ("z", *) +(* App (Lam ("x", Var "x"), *) +(* Var "z")))) in (prettify e, flag);; *) +(* - : string * bool = ("(λx.x λz.(λx.x z))", true) *) + +(* prettify ( *) +(* App ( *) +(* Lam ("x", Var "x), *) +(* Lam ("z", *) +(* App ( *) +(* Lam ("x", Var "x), *) +(* Var "z")))) *) + +(* App (Lam ("z", *) +(* Lam ("x", Var "x")), *) +(* Var "z" *) + +(* let expr, reduced = reduce_cbv (parse_string "(λx.x) (λz.(λx.x) z)") in *) +(* assert (reduced = true && *) +(* alpha_equiv expr (parse_string "λz.(λx.x) z")); *) + +(* let expr, reduced = reduce_cbv (parse_string "λz.(λx.x) z") in *) +(* assert (reduced = false && *) +(* alpha_equiv expr (parse_string "λz.(λx.x) z")); *) + +(* let expr, reduced = reduce_cbv (parse_string "(λx.y) ((λx.x x) (λx.x x))") in *) +(* assert (reduced = true && *) +(* alpha_equiv expr (parse_string "(λx.y) ((λx.x x) (λx.x x))")); *) + +(* let expr, reduced = reduce_cbv (parse_string "x y z") in *) +(* assert (reduced = false && *) +(* alpha_equiv expr (parse_string "x y z")) *) + +let rec reduce_normal e = + let e', flag = reduce_cbv e in + if flag then reduce_normal e' + else e'