Skip to content

Instantly share code, notes, and snippets.

Avatar

κeen KeenS

View GitHub Profile
View gist:9131133
$ cim for alisp ccl clisp ecl gcl sbcl do -qe '(print (expt 1.01 365))'
>>>alisp -qe (print (expt 1.01 365))
37.783386 ; Exiting
<<<
>>>ccl -qe (print (expt 1.01 365))
37.783386
<<<
>>>clisp -qe (print (expt 1.01 365))
View cl21 libs
range
datetime (date & time)
set
sortedset
queue
tree (btree)
regexp
format scanner
lazy
copy
View 1-5.v
Lemma NotNot : forall P : Prop, P -> ~~P.
Proof.
intros.
unfold not.
intros.
apply H0.
apply H.
Qed.
Require Import Classical.
View 1-1.v
Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
intros.
apply H0.
assumption.
Qed.
View 1-5.v
Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros.
split.
intro.
destruct H.
left.
apply H0.
intro.
destruct H.
View 1-2.v
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
intros.
destruct H.
intro.
apply H.
apply H0.
apply H1.
Qed.
View 1-3.v
Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
intros.
destruct H.
destruct H0.
apply H.
apply H.
Qed.
View 1-4.v
Theorem DeBolran1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
intros.
destruct H.
intro.
destruct H0.
apply H, H0.
intro.
destruct H.
destruct H0.
View 2-6.v
Require Import Arith.
Goal forall x y, x < y -> x + 10 < y + 10.
Proof.
intros.
apply plus_lt_compat_r.
apply H.
Qed.
View 2-9.v
Require Import Arith.
Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
intros.
rewrite (plus_assoc (n + m) p q).
rewrite (plus_assoc (n + p) m q).
rewrite <- (plus_assoc n m p).
rewrite <- (plus_assoc n p m).
rewrite (plus_comm m p).