Coqタクティックサンプル集

README.md

Coqタクティックサンプル集

• インデントは雑
• 証明を終わらせていないものもある

coinductive.v

(*http://adam.chlipala.net/cpdt/html/Coinductive.html*)

Require Import Lists.Streams.

(*CoFixpointでの定義*)
CoFixpoint zeroes : Stream nat := Cons 0 zeroes.
(*Lists.Streamsのconstでの定義*)
Definition ones : Stream nat := const 1.
Definition ones' := map S zeroes.

Goal EqSt ones ones'.
Proof.
  cofix.
  rewrite (unfold_Stream ones).
  rewrite (unfold_Stream ones').
  constructor.
  - simpl.
    reflexivity.
  - assumption.
Qed.

CoFixpoint bad : Stream nat := tl (Cons 0 bad).

coq_apply.v

Goal forall f: nat->Prop, (forall n: nat, f n) -> f 0.
  intros.
  apply H.
Qed.

coq_class.v

Class Sample1 := {a : nat;b : nat}.

Instance one_one : Sample1 := {a := 1;b := 1}.

Instance one_two : Sample1 := {a := 1}.
refine 2.
Qed.

Eval compute in a.

Print one_two.
Print a.

Check one_two.
Check a.

coq_coercion.v

Definition bool_in_nat (b : bool) : nat := if b then 1 else 0.
Coercion bool_in_nat : bool >-> nat.

Check true.
Check true + 1.
Eval compute in true + 1.

coq_decompose.v

Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
Proof.
  intros A B C H.
  decompose [and or] H;assumption.
Qed.

coq_destruct.v

Inductive abc (A: Prop) (B: Prop) (C: Prop): Prop :=
c1 : A -> B -> abc A B C | c2 : C -> abc A B C.

Goal forall A B C: Prop, abc A B C -> (A/\B) \/ C.
  intros.
  destruct H.
  left.
  split.
  exact H.
  exact H0.
  right.
  exact H.
Qed.

coq_evar_transitivity_instantiate_subst.v

Goal exists n : nat, forall m : nat, m = n -> m = 0.
Proof.
  evar (n' : nat).
  exists n'.
  intros.
  instantiate (1 := 0) in (Value of n').
  transitivity n'.
  assumption.
  subst n'.
  reflexivity.
Qed.

coq_exists.v

Goal forall P Q : nat->Prop, (forall n:nat, P n -> Q n) -> P 0 -> Q 0.
intros.

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex A P.

Goal forall P: nat->Prop, ex nat (fun x => P x).
intros.
exists 0.

Inductive type1 (P: nat->Prop) : Prop :=
 type1_c1 : forall n:nat, P n -> type1 P.

Goal forall P: nat->Prop, (forall n:nat, P n -> type1 P).
intro.
intros.

Goal forall (P: nat->Prop) (Q: Prop), (exists n:nat, P n) -> Q.
intros.
destruct H.


Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

Goal forall P: nat->Prop, type1 P -> exists n:nat, P n.
intros.
apply type1_c1 in H.
destruct H.

coq_implicit_and_maximally_inserted.v

Definition f {A:Type} (a:A) : A := a.
Print f.

Eval compute in (f 1).
Eval compute in (f true).

coq_inversion.v

Goal forall n : nat, n <= 0 -> n = 0.
Proof.
  intros.
  inversion H.
  reflexivity.
Qed.

Goal forall n : nat, n <= 1 -> n = 0 \/ n = 1.
Proof.
  intros.
  inversion H.
  right.
  reflexivity.
  left.
  inversion H1.
  reflexivity.
Qed.

coq_monad.v

(* http://yosh.hateblo.jp/entry/20090904/p1 *)

Class HMonad (M: Type -> Type) := {
  (* fields *)
   mreturn : forall {A}, A -> M A
 ; mbind : forall {A B}, M A -> (A -> M B) -> M B
  (* axioms モナド則 *)
 ; left_identity : forall A B (a: A) (f: A -> M B), mbind (mreturn a) f = f a
 ; right_identity : forall A (m: M A), mbind m mreturn = m
 ; associativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C),
       mbind (mbind m f) g = mbind m (fun x => mbind (f x) g)
}.

Print option.

Instance Maybe: HMonad option := {
   mreturn A x := Some x
 ; mbind A B m f :=
     match m with
     | None => None
     | Some x => f x
     end
}.

intros.
reflexivity.

intros.
case m;reflexivity.

intros.
case m;[|reflexivity].
intros.
case (f a);reflexivity.
Qed.

Print list.

Require Import Coq.Lists.List.

Instance List : HMonad list := {
  mreturn A x := (x::nil)%list
 ;mbind A B m f := flat_map f m
(* ;mbind A B m f := (fix mbind' l f :=
    match l with
    | nil => nil
    | x::l' => (f x) ++ mbind' l' f
    end) m f*)
}.
{
intros.
simpl.
rewrite <- app_nil_end.
reflexivity.
}
{
intros.
induction m.
- simpl.
  reflexivity.
- simpl.
  f_equal.
  assumption.
}

Lemma l1 : forall (A B: Type) (f:A->list B) (l m:list A), flat_map f (l ++ m) = flat_map f l ++ flat_map f m.
  intros.
  induction l.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHl.
    apply app_assoc.
Qed.

{
intros.
induction m.
- simpl.
  reflexivity.
- simpl.
  rewrite l1.
  f_equal.
  assumption.
}

coq_Print.v

Print ML Path.
Print Libraries.
Print LoadPath.
Print Ltac exfalso.
Print HintDb bool.

Locate and.

Section Sec1.
  Print Section Sec1.
  Section Sec2.
    Print Section Sec1.
    Print Section Sec2.
  End Sec2.
End Sec1.

Print Visibility.
Print Scopes.

Print Scope list_scope.
Print Scope nat_scope.

Require Import Reals.
Print Scope R_scope.

coq_record.v

Record Rat : Set := mkRat {
  numer : nat;
  denom : nat;
  denom_not_zero : denom <> O;
  irreducible : forall g n d:nat, 
    (mult g n)=numer /\ (mult g d)=denom -> g = S O
}.

Print numer.

Lemma two_not_zero : 2 <> 0.
Proof.
  discriminate.
Qed.
Lemma one_two_irred : forall g n d:nat, (mult g n)=1 /\ (mult g d)=2 -> g = S O.
Admitted. 

Definition half : Rat := mkRat 1 2 two_not_zero one_two_irred.
Print half. (* mkRat 1 2 two_not_zero one_two_irred : Rat *)
Eval compute in (numer half). (* 1 : nat *)
Eval compute in (denom_not_zero half). (* two_not_zero *)

coq_rename.v

Goal forall P:Prop, P -> P.
Proof.
  intros.
  rename H into h.
  apply h.
Qed.

coq_section.v

Section sec1.
  Variable A :Prop.
  Definition f (B:Prop) : Prop := A -> B.
  Print Section sec1.
End sec1.

Print f.

coq_set.v

Goal 0 = 0.
  set 0.
  reflexivity.
Qed.

coq_split.v

Inductive and3 (A:Prop) (B:Prop) (C:Prop) : Prop :=
conj3: A -> B -> C -> and3 A B C.

Goal forall P Q R : Prop, P->Q->R->and3 P Q R.
Proof.
  intros.
  split.
    assumption.
    assumption.
    assumption.
Qed.

dependent_induction.v

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
  intros n H.
  induction H.
Print lt.
Print le.
Abort.

Require Import Coq.Program.Equality.

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
  intros n H.
  dependent induction H.
  - reflexivity.
  - inversion H.
Qed.

lia_psatzl.v

Require Import Psatz.
Require Import ZArith.
Require Import Reals.

Open Scope Z_scope.

Goal forall x y, 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False.
Proof.
  intros.
  lia.
Qed.

Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
Proof.
  intros.
  lia.
Qed.

(*http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Micromega/trunk*)

Close Scope Z_scope.

Open Scope R_scope.

Lemma yplus_minus : forall x y,
  0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y.
Proof.
  intros.
  psatzl R.
Qed.

ltac.v

Print Ltac exfalso.

Ltac f x :=
match x with
  context f [S ?X] => 
  idtac X;                    (* To display the evaluation order *)
  assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
  let x:= context f[O] in assert (x=O) (* To observe the context *)
end.

Goal True.
  f (5).
Abort.

Ltac g :=
match goal with
  | _:?X |- (?X /\ ?X) => split;assumption
end.

Ltac g1 :=
match goal with
  | h:?X |- (?X /\ ?X) => split;apply h
end.

Ltac g2 :=
match goal with
  | h1:?X, h2:?Y |- (?X /\ ?Y) => split;[apply h1|apply h2]
end.

Goal forall P:Prop, P -> P /\ P.
  intros.
  g.
Qed.

Goal forall P:Prop, P -> P /\ P.
  intros.
  g.
Qed.

Goal forall P Q:Prop, Q -> P -> P /\ Q.
  intros.
  g2.
Qed.

Scheme.v

Variables A B : Set.

Inductive tree : Set :=
    node : A -> forest -> tree
with forest : Set :=
  | leaf : B -> forest
  | cons : tree -> forest -> forest.

Scheme tree_forest_rec := Induction for tree Sort Set
  with forest_tree_rec := Induction for forest Sort Set.


Check tree_forest_rec.
Check forest_tree_rec.

(*https://coq.inria.fr/refman/Reference-Manual016.html*)

(*Functional Schemeについては*)
(*http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt7.html*)

Scope.v

Locate "_ = _".
Locate "exists".

Print Scopes.
Print Visibility.

Parameter U : Set.

Bind Scope U_scope with U.

Parameter Uplus : U -> U -> U.

Infix "+" := Uplus : U_scope.

Locate "+".

Delimit Scope U_scope with U_key.

Goal forall a b : U, (a + b = a + b)%U_key.
Abort.

Open Scope U_scope.

Print Visibility.

Goal forall a b : U, a + b = a + b.
Abort.

Close Scope U_scope.

Print Visibility.

Print Grammar constr.