ryuta-ito
10/29/2018 - 12:34 PM
coq_notation.md
sigma type
Require Import Omega.
Print sig. (* Σx:A B(x) *)
(* Inductive sig (A : Type) (P : A -> Prop) : Type := *)
(* exist : forall x : A, P x -> {x : A | P x} *)
(* For sig: Argument A is implicit *)
(* For exist: Argument A is implicit *)
Check sig (fun x:nat => x < 10).
(* {x : nat | x < 10} *)
(* : Set *)
Check {x:nat | x < 10}.
(* {x : nat | x < 10} *)
(* : Set *)
Lemma _2_lt_10 : 2 < 10. Proof. omega. Qed.
Check exist (fun n:nat => n < 10) 2 _2_lt_10.
(* exist (fun n : nat => n < 10) 2 _2_lt_10 *)
(* : {n : nat | n < 10} *)
(* exist <P of predicate> <x of argument> <proof object of P x>. *)
Co-Inductive
Set Implicit Arguments.
Unset Strict Implicit.
Section Stream.
Variable A : Type.
CoInductive Stream : Type :=
Seq : A -> Stream -> Stream.
Definition hd (x : Stream) :=
match x with
| Seq a _ => a
end.
Definition tl (x : Stream) :=
match x with
| Seq _ s => s
end.
Fixpoint nth (n : nat) (x : Stream) : A :=
match n with
| O => hd x
| S m => nth m (tl x)
end.
Fixpoint take (n : nat) (x : Stream) : list A :=
match n with
| O => nil
| S m => cons (hd x) (take m (tl x))
end.
Fixpoint drop (n : nat) (s : Stream) : Stream :=
match n with
| O => s
| S m => drop m (tl s)
end.
End Stream.
CoFixpoint from (n : nat) : Stream nat := Seq n (from (S n)).
Eval compute in hd (from 0).
(* = 0 *)
(* : nat *)
Eval compute in tl (from 0).
(* = (cofix from (n : nat) : Stream nat := Seq n (from (S n))) 1 *)
(* : Stream nat *)
Eval compute in nth 10 (from 0).
(* = 10 *)
(* : nat *)
Eval compute in take 10 (from 0).
(* = (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)%list *)
(* : list nat *)
Eval compute in drop 10 (from 0).
(* = (cofix from (n : nat) : Stream nat := Seq n (from (S n))) 10 *)
(* : Stream nat *)
Record
implicit
Set Implicit Arguments.
Unset Strict Implicit.
Structure hoge := {
carrier : Type;
op : carrier -> carrier
}.
Definition fuga := Build_hoge (plus 1).
Eval simpl in carrier fuga.
(* = nat *)
(* : Type *)
Canonical Structure fuga.
Check op 1.
(* op (h:=fuga) 1 *)
(* : carrier fuga *)
Definition style
Canonical Structure piyo := Build_hoge (plus 1).
Check op 1.
(* op (h:=piyo) 1 *)
(* : carrier piyo *)
explicit
Record hoge := {
carrier : Type;
op : carrier -> carrier
}.
Definition fuga := Build_hoge _ (plus 1).
Check op fuga 1.
(* op fuga 1 *)
(* : carrier fuga *)
Fail Check op _ 1.
(* The command has indeed failed with message: *)
(* The term "1" has type "nat" while it is expected to have type "carrier ?h". *)
Canonical Structure fuga.
Check op _ 1.
(* op fuga 1 *)
(* : carrier fuga *)
:>
Set Implicit Arguments.
Unset Strict Implicit.
Structure Fuga : Type := {
Carrier_ : Set
}.
Fail Check forall (f : Fuga) (carrier : f), carrier = carrier.
(* The term "f" has type "Fuga" which should be Set, Prop or Type. *)
Structure Hoge : Type := {
Carrier :> Set
}.
Print Carrier.
(* Carrier = fun h : Hoge => let (Carrier) := h in Carrier *)
(* : Hoge -> Set *)
(* Carrier is a coercion *)
Check forall (A : Hoge) (carrier : A), carrier = carrier.
(* forall (A : Hoge) (carrier : A), carrier = carrier *)
(* : Prop *)
Set Printing Coercions.
Check forall (A : Hoge) (carrier : A), carrier = carrier.
(* forall (A : Hoge) (carrier : Carrier A), carrier = carrier *)
(* : Prop *)
Ltac
Ltac asdf := reflexivity.
Definition hogge : 1 = 1.
Proof.
asdf.
Qed.
of
Definition hoge of nat := 19.
Eval compute in hoge 99.
(* = 19 *)
(* : nat *)
Coercion
Definition nat_to_bool (_ : nat) := true.
Coercion nat_to_bool : nat >-> bool.
Check (andb 10 true).
(* (10 && true)%bool *)
(* : bool *)
Set Printing Coercions.
Check (andb 10 true).
(* (nat_to_bool 10 && true)%bool *)
(* : bool *)
(* Definition style *)
Coercion foo (_:bool) := 10.
Check plus 10 true.
(* 10 + foo true *)
(* : nat *)
Print Graph.
(* [nat_to_bool] : nat >-> bool *)
(* [foo] : bool >-> nat *)
Coercion path
Inductive hoge := Hoge.
Inductive fuga := Fuga.
Inductive piyo := Piyo.
Coercion fuga_of_hoge (h:hoge) := Fuga.
Coercion piyo_of_fuga (f:fuga) := Piyo.
Print Graph.
(* [fuga_of_hoge] : hoge >-> fuga *)
(* [fuga_of_hoge; piyo_of_fuga] : hoge >-> piyo *)
(* [piyo_of_fuga] : fuga >-> piyo *)
Set Printing Coercions.
Check Hoge : piyo.
(* piyo_of_fuga (fuga_of_hoge Hoge) : piyo *)
(* : piyo *)
Eval hnf in (fun p:piyo => p) Hoge.
(* = Piyo *)
(* : piyo *)
Eval hnf in (fun p:hoge => p:piyo) Hoge.
(* = Piyo *)
(* : piyo *)
Applicative style
Inductive hoge := Hoge.
Definition fun_of_hoge (h:hoge) := fun (h:hoge) => h.
Coercion fun_of_hoge : hoge >-> Funclass.
Set Printing Coercions.
Check Hoge Hoge.
(* fun_of_hoge Hoge Hoge *)
(* : hoge *)
Check Hoge Hoge Hoge Hoge Hoge Hoge Hoge Hoge.
(* fun_of_hoge *)
(* (fun_of_hoge *)
(* (fun_of_hoge *)
(* (fun_of_hoge *)
(* (fun_of_hoge (fun_of_hoge (fun_of_hoge Hoge Hoge) Hoge) Hoge) Hoge) *)
(* Hoge) Hoge) Hoge *)
(* : hoge *)
Eval hnf in Hoge Hoge.
(* = Hoge *)
(* : hoge *)
let
Eval compute in let a := 10 in a.
(* = 10 *)
(* : nat *)
Inductive hoge :=
| fuga : forall (n:nat), hoge.
Eval simpl in let 'fuga n := fuga 10 in n.
(* = 10 *)
(* : nat *)