Skip to content

Instantly share code, notes, and snippets.

@risou
Created May 11, 2011 05:39
Show Gist options
  • Save risou/965984 to your computer and use it in GitHub Desktop.
Save risou/965984 to your computer and use it in GitHub Desktop.
coqt2
Definition prop0 : forall (A : Prop), A -> A.
Proof.
intros.
apply H.
Qed.
Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.
Proof.
intro.
intro.
intro.
intro.
apply H0.
intro.
apply (H (P -> Q)).
apply (H P).
Qed.
Goal forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R.
intros.
apply H0.
apply H.
apply H1.
Qed.
(* リスト定義
Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.
*)
Goal forall P : Prop, P -> ~~P.
intros.
intro.
apply H0.
apply H.
Qed.
Goal forall (P Q : Prop), P \/ Q -> Q \/ P.
intros.
case H.
apply or_intror.
apply or_introl.
Qed.
Goal forall (P Q : Prop), P /\ Q -> Q /\ P.
intros.
destruct H.
apply conj.
apply H0.
apply H.
Qed.
Goal forall (P : Prop), ~(P /\ ~P).
intros.
intro.
destruct H.
apply H0.
apply H.
Qed.
Goal forall (P Q : Prop), ~P \/ ~Q -> ~(P /\ Q).
intros.
intro.
destruct H.
destruct H0.
apply H.
apply H0.
destruct H0.
apply H.
apply H1.
Qed.
Goal forall (P : Prop), (forall (P : Prop), ~~P -> P) -> P \/~P.
intros.
apply H.
unfold not.
intros.
apply H0.
right.
intro.
apply H0.
left.
apply H1.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment