add few old coq files

README.org

@@ -0,0 +1,24 @@
+#+TITLE: README
+
+ - haskell
+ - sml
+ - agda
+ - coq
+ - pvs
+
+ - apl
+ - c
+ - cpp
+ - rust
+
+ - python
+ - lua
+ - bash
+
+ - nusmv
+ - risc-v
+
+ - verilog
+ - vhdl
+
+ - misc

coq/README.org

@@ -6,9 +6,13 @@
  - [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes.
  - [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws
  - [[./odd-even-prop.v][odd-even-prop.v]]: Parity of ~nat~ values
+ - [[./ltac2-demo.v][ltac2-demo.v]]: 'Hello world' with Ltac2
+ - [[./inf-proof.v][inf-proof.v]]: A trivial proof involving streams (ie, infinite lists)
+ - [[./3-way-mutrec.v][3-way-mutrec.v]]: An example of a 3-way mutually recursive function
+ - [[./iseven-proof-mode.v][iseven-proof-mode.v]]: An ~iseven~ function defined only using proof mode
  - [[./cpdt/][cpdt/]]: stuff from the book CPDT
-   + [[./cpdt/ilist.v][cpdt/ilist.v]]: Length indexed lists
-   + [[./cpdt/exercises.v][cpdt/exercises.v]]: a few of the old exercises from cpdt
+   + [[./cpdt/ilist.v][ilist.v]]: Length indexed lists
+   + [[./cpdt/exercises.v][exercises.v]]: a few of the old exercises from cpdt
  - [[./sf/][sf]]: stuff from /Software foundations/
  - [[./third-party/][Snippets using third party libraries]]
    + [[./third-party/eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin

coq/cpdt/ilist.v

@@ -114,6 +114,18 @@ Qed.
 (* Well... that was easier than what I expected..
    Dependent types do pay off, I guess.. *)
 
+Require List.
+Fixpoint listToIlist {A:Type} (l:list A): ilist A (List.length l) :=
+  match l with
+  | List.nil => INil
+  | List.cons x xs => ICons x (listToIlist xs)
+  end.
+
+Fixpoint ilistToList {A:Type} {n:nat} (l:ilist A n): list A :=
+  match l with
+  | INil => nil
+  | ICons x xs => List.cons x (ilistToList xs)
+  end.
 
 Module IListNotations.
   Declare Scope ilist_scope.
@@ -144,3 +156,12 @@ Compute iget [1; 2] (Next First).
 (* = 2 : nat *)
 Fail Compute iget [1; 2] (Next (Next First)).
 
+
+Compute listToIlist (cons 3 (cons 2 (cons 1 (cons 0 nil)))).
+(* = [3; 2; 1; 0]
+     : ilist nat (length (3 :: 2 :: 1 :: 0 :: nil))
+ *)
+Compute ilistToList (listToIlist (cons 3 (cons 2 (cons 1 (cons 0 nil))))).
+(* = (3 :: 2 :: 1 :: 0 :: nil)%list
+     : list nat
+*)

coq/inf-proof.v

@@ -0,0 +1,48 @@
+Require Import Streams.
+
+CoInductive stream_eq {A:Type} : Stream A -> Stream A -> Prop :=
+| Stream_eq : forall (h:A) (tl1 tl2:Stream A),
+    stream_eq tl1 tl2 -> stream_eq (Cons h tl1) (Cons h tl2).
+
+CoFixpoint zeros : Stream nat := Cons 0 zeros.
+CoFixpoint ones : Stream nat := Cons 1 ones.
+Definition ones' := map S zeros.
+
+Definition sUnfold {A:Type} (s:Stream A) : Stream A :=
+  match s with
+  | Cons x xs => Cons x xs
+  end.
+
+
+(* From Pierre Castéran *)
+Lemma stm_unfold {A: Type} (s: Stream A) :
+    s = match s with Cons a s' => Cons a s' end.
+Proof.
+    now destruct s.
+Qed.
+
+Inductive starts_with {A: Type} (a:A): Stream A -> Prop :=
+        starts_hd : forall s, starts_with a (Cons a s).
+
+Goal Streams.Exists (starts_with 3) (const 3).
+  left; rewrite (stm_unfold (const 3)); split.
+Qed.
+
+Goal Streams.Exists (starts_with 3) (Cons 4 (const 3)).
+  right; left.
+  rewrite (stm_unfold (const 3)).
+  split.
+Qed.
+
+
+(*
+   By the way, here's an infinite list
+
+   This is like `foo = 3 : foo` in Haskell.
+*)
+CoFixpoint incStream (n:nat):Stream nat :=
+  Cons n (incStream (S n)).
+
+
+Compute Streams.hd (Streams.tl (incStream 1)).
+

coq/iseven-proof-mode.v

@@ -0,0 +1,8 @@
+Fixpoint iseven (n:nat): bool.
+Proof.
+  induction n.
+  - exact true.
+  - destruct n.
+    * exact false.
+    * exact (iseven n).
+Defined.

coq/ltac2-demo.v

@@ -0,0 +1,198 @@
+(*
+Thanks to Yiyun Liu.
+ *)
+
+(*
+https://github.com/coq/coq/blob/master/user-contrib/Ltac2/
+ *)
+
+From Ltac2 Require Import Ltac2.
+
+(* Int is a primitive datatype in ltac2 *)
+Ltac2 Eval 1.
+Ltac2 Eval Int.add 1 2.
+
+(* Lambda *)
+Ltac2 Eval (fun x => x).
+Ltac2 Eval (fun x => Int.add x x).
+Ltac2 Eval (fun x => Int.add x x) 5.
+
+(* let binding *)
+Ltac2 Eval let f := (fun x => Int.add x x) in f 5.
+
+(* An ltac2 function *)
+Ltac2 double_int := (fun x => Int.add x x).
+Ltac2 Eval double_int 4.
+
+(* Syntactic sugar for the above *)
+Ltac2 double_int2 x := Int.add x x.
+Ltac2 Eval double_int2 4.
+
+(* Type annotations also possible *)
+Ltac2 double_int3 (x:int) := Int.add x x.
+
+(* Like ltac1, no termination check *)
+(*
+Ltac2 is_even x := Int.equal (Int.mod x 2).
+
+Ltac2 rec collatz n := 
+  if Int.le n 1 then 0
+  else  
+ *)
+(* TODO: Comment lines in emacs *)
+
+(* ALlgebraic datateyp *)
+Ltac2 Type rec PNat :=
+  [ Z | S (PNat) ].
+
+Ltac2 rec padd (m:PNat) (n:PNat) :=
+  match m with
+  | Z => n
+  | S m' => S (padd m' n)
+  end.
+
+(* Looks like a less powerful version of ocaml *)
+Ltac2 Type rec 'a Tree :=
+  [ Empty | Node ('a, 'a Tree, 'a) ].
+
+(* No deptypes in ltac2 *)
+Fail Ltac2 rec treeSize (t: 'a Tree) :=
+  match t with
+  | Empty => 0
+  | Node l v r => Int.add 1 (Int.add (treeSize l) (treeSize r))
+  end.
+
+Ltac2 Eval '1. (* Gallina term ! *)
+Ltac2 Eval '(1,2). (* Gallina term ! *)
+
+Ltac2 Type ('a, 'b) Pair := { fst: 'a; snd: 'b }.
+Ltac2 Eval {fst:=1; snd:=2}.
+Ltac2 Eval  {fst:=1; snd:=2}.(fst).
+
+(* We can refer to Gallina top-level defns *)
+Definition four := 4.
+Ltac2 Eval 'four.
+
+(* ' is like constr: in ltac1 *)
+
+Ltac2 Eval (1,true).
+
+Fail Ltac2 Eval four. (* Fails because not an ltac2 variable *)
+Fail Ltac2 Eval fst (1,2). (* TODO *)
+
+Ltac2 Eval Int.le 2 3.
+
+(* Gallina term! *)
+Ltac2 rec int_n n :=
+  match Int.le n 0 with
+  | true => '0
+  | false =>
+      let n' := int_n (Int.sub n 1) in
+      '(1 + $n')  (* The $ is like the ' in lisp *)
+  end.
+Ltac2 Eval int_n 2.
+(* - : constr = constr:(1 + (1 + 0)) *)
+
+(* The constructed Gallina terms won't be evaluated. So no type checking *)
+Ltac2 rec int_n2 n :=
+  match Int.le n 0 with
+  | true => 'true
+  | false =>
+      let n' := int_n (Int.sub n 1) in
+      '(1 + $n')  (* The $ is like the ' in lisp *)
+  end.
+
+
+Ltac2 Eval Constr.equal '(fun x:nat => x) '(fun z:nat => z).
+(* - : bool = true *)
+
+(* No type annotations => somethign like evar might show up. ie, holes *)
+Ltac2 Eval Constr.equal '(fun x => x) '(fun z:nat => z).
+(* - : bool = false *)
+
+Ltac2 Eval Constr.equal '(1 + 1) '2.
+(* - : bool = false *)
+
+Ltac2 Eval Constr.equal '(1 + 1) (int_n 1).
+(* - : bool = false *)
+
+
+(* Querying proof state *)
+Ltac2 Eval Control.hyps.
+Ltac2 Eval Control.hyps ().
+
+Section foo.
+  Variable x : nat.
+  Ltac2 Eval Control.hyps ().
+(*
+- : (ident * constr option * constr) list = [(@x, None, constr:(nat))]
+*)
+
+  Variable y : nat.
+  Ltac2 Eval Control.hyps ().
+(*
+- : (ident * constr option * constr) list = [(@x, None, constr:(nat));
+(@y, None, constr:(nat))]
+*)
+
+  Parameter z : nat. (* Not change in hyps! *)
+  Ltac2 Eval Control.hyps ().
+(*
+- : (ident * constr option * constr) list = [(@x, None, constr:(nat));
+(@y, None, constr:(nat))]
+*)
+End foo.
+
+
+Module modfoo.
+  Parameter x : nat.
+  Ltac2 Eval Control.hyps ().
+  (* - : (ident * constr option * constr) list = [] *)
+End modfoo.
+
+Ltac2 Eval Control.enter (fun _ => Control.goal (); ()).
+Ltac2 Eval Control.enter.
+
+(*************POST*************)
+(* Mutable cells *)
+Ltac2 mutable x_mut := 3.
+Ltac2 Eval x_mut.
+Ltac2 Set x_mut := 2.
+Ltac2 Eval x_mut.
+
+Ltac2 x_immut := 3.
+Fail Ltac2 Set x_immut := 2.
+(* The tactic x_immut is not declared as mutable *)
+
+(* Can access old value of a mutable variable with [as] *)
+Ltac2 mutable f x := Int.add x 1.
+Ltac2 Eval f 3.  (* 4 *)
+
+Ltac2 Set f as oldf := fun x => Int.add 10 (oldf x).
+Ltac2 Eval f 3.  (* 14 *)
+
+
+(*********** Printing **********)
+
+From Ltac2 Require Import Message.
+Fail Message.print (Message.of_string "unqualified calls").
+Fail Message.print '(1 + 1).
+
+Fail Ltac2 Eval Int.mod 2 3.
+(* Gives a list of hypotheses *)
+
+(* TODO:
+ - Is it possible to mix ltac1 and ltac2
+ - Where to find ltac2 docs
+ - How usable is ltac2 at the moment? Maturity-wise? Earlier something being buggy (auto?) was mentioned. 
+ - ast print of gllaina term constructed there's a pirnt function or something in library as string 
+   + there is something int to string
+   + Gives your more control in some sense. You can get out when you want.
+
+ - semicolon is different in ltac2. got to iterate manually or something
+ - auto is buggy in ltac2?
+ - Ltac2 have states?
+ - https://coq.inria.fr/refman/proof-engine/ltac2.html#coq:tacn.lazy_match!
+ - evar is a goal, but all goals aren't evar?? said by Irene Yoon??
+   *)
+

coq/third-party/extlib-hlist.v

@@ -1,5 +1,7 @@
 (* coq-ext-lib *)
 
+(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
+(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.Member.html *)
 From ExtLib Require Import HList.
 
 Module HListNotations.
@@ -26,6 +28,7 @@ Check «3; true» : hlist (fun x:Set=>x) [nat; bool].
 Example eg1 := «3» : hlist (fun x:Set=>x) [nat]. 
 Example eg2 := «2; true»: hlist (fun x:Set=>x) [nat; bool]. 
 Example eg3 := «(0,3)» : hlist (fun x:Set=>(x*nat)%type) [nat]. 
+Example eg4 := «2; true; "h"; (2,3)»: hlist (fun x:Set=>x) [nat; bool; string; (nat*nat)%type]. 
 
 
 Check «» : hlist (fun x:Set=>x) [].
@@ -59,13 +62,40 @@ From ExtLib Require Import Member.
 (* Kinda like the relation between [sumbool] and [bool] *)
 Print member.
 
-Lemma pf1 : member nat [nat]. constructor. Qed.
-Lemma pf2 : member nat [nat; bool]. constructor. Qed.
-Print pf1.
+(** Indexing *)
+Compute hlist_get (MZ _ _) eg2.
+(* = 2 : nat *)
+Compute hlist_get (MN _ (MZ _ _)) eg2.
+(* = true : bool *)
+Compute hlist_get (MN _ (MN _ (MZ _ _))) eg4.
+(* = "h" : string *)
+Compute hlist_get (MN _ (MN _ (MN _ (MZ _ _)))) eg4.
+(* = (2, 3) : nat * nat *)
 
-Check hlist_get pf1 eg1.
-Compute hlist_get pf1 eg1.
-Check hlist_get (pf1:member nat _) eg1.
-Compute hlist_get (pf1:member nat _) eg1.
-Compute S (hlist_get (pf1:member nat _) eg1).
-Compute (hlist_get (pf2:member nat _) eg2).
+(** Getting nth element *)
+Compute hlist_nth eg4 2.
+(* = "h"
+     : match nth_error [nat; bool; string; (nat * nat)%type] 2 with
+       | Some t => t
+       | None => unit
+       end
+*)
+
+Compute nth_error[nat; bool; string; (nat * nat)%type] 2.
+(* = Some string : option Set *)
+
+Unset Printing Notations.
+
+(** Converting list to hlist ?? *)
+Compute hlist_gen _ [1].
+(* = Hcons (?f 1) Hnil
+     : hlist ?F (cons 1 nil) *)
+
+Compute hlist_gen (fun x=>x) [1].
+(* = Hcons 1 Hnil
+     : hlist (fun _ : nat => nat) (cons 1 nil) *)
+
+
+(** Converting hlist to list ?? *)
+(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
+Fail Check hlist_erase eg1.

misc/README.org

@@ -5,3 +5,6 @@ ACL2 proof assistant:
 
 Maude model cheker:
  - my-nat.maude
+
+minlog:
+ - minlog-hello.scm

misc/minlog-hello.scm

@@ -0,0 +1,60 @@
+; Execute current line (cursor placed after closing parenthesis): C-x C-e
+; Execute region: C-c C-r
+; undo: (undo) or (undo n)
+; End scheme session: (exit)
+;
+; ----------------------------------------------------
+;
+; Parenthesis associate to right
+;
+; (A -> (B -> C)) -> ((A -> B) -> (A -> C))
+;
+; which is same as
+;
+; (A -> B -> C) -> (A -> B) -> (A -> C)
+;
+; ----------------------------------------------------
+; ; Writing the formula:
+;
+; Declare predicate variables A, B, C
+(add-pvar-name "A" "B" "C" (make-arity))
+; Minlog output:
+;> ok, predicate variable A: (arity) added
+;ok, predicate variable B: (arity) added
+;ok, predicate variable C: (arity) added
+
+(set-goal "(A -> B -> C) -> (A -> B) -> (A -> C)")
+; Minlog output:
+;----------------------------------
+; ?_1:(A -> B -> C) -> (A -> B) -> A -> C
+
+; Assume (A -> B -> C)
+(assume 1)
+; Minlog output:
+;> ok, we now have the new goal 
+;
+;  1:A -> B -> C
+;----------------------------------
+;?_2:(A -> B) -> A -> C
+
+; Assume (A -> B)
+(assume 2)
+; Minlog output:
+;> ok, we now have the new goal 
+;
+;  1:A -> B -> C
+;  2:A -> B
+;----------------------------------
+;?_3:A -> C
+
+
+; Assume A
+(assume 3)
+; Minlog output:
+;> ok, we now have the new goal 
+;
+;  1:A -> B -> C
+;  2:A -> B
+;  3:A
+;----------------------------------
+;?_4:C