Last active
August 29, 2015 14:02
-
-
Save joisino/171da64ef8c4a9875a36 to your computer and use it in GitHub Desktop.
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
Ltac split_all := repeat try split. | |
(* 以下は動作確認用 *) | |
Lemma bar : | |
forall P Q R S : Prop, | |
R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q). | |
Proof. | |
intros P Q R S H0 H1 H2 H3. | |
split_all. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
Qed. | |
Lemma baz : | |
forall P Q R S T : Prop, | |
R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T. | |
Proof. | |
intros P Q R S T H0 H1 H2 H3 H4. | |
split_all. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
Qed. | |
Lemma quux : | |
forall P Q : Type, P -> Q -> P * Q. | |
Proof. | |
intros P Q H0 H1. | |
split_all. | |
- assumption. | |
- assumption. | |
Qed. | |
Record foo := { | |
x : (False -> False) /\ True /\ (False -> False); | |
y : True; | |
z : (False -> False) /\ True | |
}. | |
Lemma hogera : foo. | |
Proof. | |
split_all. | |
- intros H; exact H. | |
- intros H; exact H. | |
- intros H; exact 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
Require Import Arith. | |
Require Import Omega. | |
Require Import Recdef. | |
Function log(n:nat) {wf lt n} := | |
if le_lt_dec n 1 then | |
0 | |
else | |
S (log (Div2.div2 n)). | |
Proof. | |
intros. | |
apply Div2.lt_div2. | |
omega. | |
apply lt_wf. | |
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
Ltac split_all := | |
match goal with | |
| |- (_ /\ _) => try split;split_all | |
| |- _ => idtac | |
end. | |
(* 以下は動作確認用 *) | |
Lemma bar : | |
forall P Q R S : Prop, | |
R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q). | |
Proof. | |
intros P Q R S H0 H1 H2 H3. | |
split_all. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
Qed. | |
Lemma baz : | |
forall P Q R S T : Prop, | |
R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T. | |
Proof. | |
intros P Q R S T H0 H1 H2 H3 H4. | |
split_all. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
- assumption. | |
Qed. | |
Lemma quux : | |
forall P Q : Type, P -> Q -> P * Q. | |
Proof. | |
intros P Q H0 H1. | |
split_all. | |
split. | |
- assumption. | |
- assumption. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment