This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ 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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
range | |
datetime (date & time) | |
set | |
sortedset | |
queue | |
tree (btree) | |
regexp | |
format scanner | |
lazy | |
copy |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q. | |
Proof. | |
intros. | |
apply H0. | |
assumption. | |
Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P. | |
Proof. | |
intros. | |
destruct H. | |
intro. | |
apply H. | |
apply H0. | |
apply H1. | |
Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q. | |
Proof. | |
intros. | |
destruct H. | |
destruct H0. | |
apply H. | |
apply H. | |
Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Lemma NotNot : forall P : Prop, P -> ~~P. | |
Proof. | |
intros. | |
unfold not. | |
intros. | |
apply H0. | |
apply H. | |
Qed. | |
Require Import Classical. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q. | |
Proof. | |
intros. | |
split. | |
intro. | |
destruct H. | |
left. | |
apply H0. | |
intro. | |
destruct H. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Arith. | |
Goal forall x y, x < y -> x + 10 < y + 10. | |
Proof. | |
intros. | |
apply plus_lt_compat_r. | |
apply H. | |
Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Goal forall P Q : nat -> Prop, P 0 -> (forall x , P x -> Q x) -> Q 0. | |
Proof. | |
intros. | |
apply H0. | |
apply H. | |
Qed. | |
Goal forall P : nat -> Prop, P 2 -> (exists y, P (1 + y)). | |
Proof. | |
intros. |
OlderNewer