Library twenty_tautologies
This is a training file before H3.Q5 (non-constructive tautologies).
We cover not just the non-constructive stuff (axioms classic and NNPP, but many other tactics used in tautologies.
Lemma sample1: forall a b: Prop, ~a -> a -> b.
Proof.
intros a b.
unfold not.
intros aFalse.
intros aTrue.
pose (aFalse aTrue) as H2.
contradiction H2.
Qed.
Proof.
intros a b.
unfold not.
intros aFalse.
intros aTrue.
pose (aFalse aTrue) as H2.
contradiction H2.
Qed.
Same proof, just a bit shorter
Lemma sample1_VAR: forall a b: Prop, ~a -> a -> b.
Proof.
intros a b.
unfold not.
intros aFalse aTrue.
contradiction (aFalse aTrue).
Qed.
Proof.
intros a b.
unfold not.
intros aFalse aTrue.
contradiction (aFalse aTrue).
Qed.
Note: You cannot switch 'aFalse' and 'aTrue' in the last line.
The following will not be accepted:
Intuition: If a=True, but b=False, then implication (a ->b) is always False.
contradiction (aTrue aFalse).Modus ponens cannot insert '(a -> False)' into expression 'a', but it can insert 'a' into '(a -> False)' to get 'False', a contradiction.
Lemma sample2: forall a b: Prop, a -> (~b -> ~(a -> b)).
Proof.
intros a b.
unfold not.
intros aTrue bFalse.
intros H.
apply bFalse.
apply H.
apply aTrue.
Qed.
Proof.
intros a b.
unfold not.
intros aTrue bFalse.
intros H.
apply bFalse.
apply H.
apply aTrue.
Qed.
Note: In this example we reasoned 'backwards' with three 'apply' tactics.
Same proof written shorter
- replaced the goal False by 'b',
- replaced the goal 'b' by 'a',
- finally, we know that 'a' is true.
Lemma sample2_VAR: forall a b: Prop, a -> (~b -> ~(a -> b)).
Proof.
unfold not.
intros a b aTrue bFalse H.
apply (bFalse (H aTrue)).
Qed.
Proof.
unfold not.
intros a b aTrue bFalse H.
apply (bFalse (H aTrue)).
Qed.
The last line works just like function composition.
In most programming languages we would write function calls like this:
The last goal is False; so it is also a contradiction
In most programming languages we would write function calls like this:
bFalse(H(aTrue))But in Coq syntax function call is an expression in parentheses: The first item is the function/implication name. After that there is one or more arguments.
Lemma sample2_VARVAR: forall a b: Prop, a -> (~b -> ~(a -> b)).
Proof.
unfold not.
intros a b aTrue bFalse H.
contradiction (bFalse (H aTrue)).
Qed.
Proof.
unfold not.
intros a b aTrue bFalse H.
contradiction (bFalse (H aTrue)).
Qed.
Non-constructive stuff
Require Import Classical_Prop.
Intuition: If implication (a -> b) is False, then 'a' must be True
Lemma sample3: forall a b: Prop, ~(a -> b) -> a.
Proof.
intros a b H1.
apply NNPP.
unfold not.
intro H2.
apply H1.
intro aTrue.
contradiction (H2 aTrue).
Qed.
Proof.
intros a b H1.
apply NNPP.
unfold not.
intro H2.
apply H1.
intro aTrue.
contradiction (H2 aTrue).
Qed.
Using the tactic
Type this to display meaning of this symbol
apply NNPPadds two negations to the goal. The axiom NNPP reads like this: ~~a -> a, one can reason backwards. Such step provides additional possibilities to do non-constructive proofs by contradiction whenever we are stuck.
Print NNPP.
Note: The lemma NNPP (just like the lemmas that
we are doing is, in fact, a function.
It eats one parameter and (after some body) produces 'usable stuff':
~~p -> p.
Intuition: If both 'a' and 'b' are False, then the disjunction 'a \/ b' is False
Lemma sample4: forall a b: Prop, ~a -> ~b -> ~(a \/ b).
Proof.
intros a b.
unfold not.
intros aFalse bFalse.
intros aORb.
destruct aORb as [aTrue | bTrue].
contradiction (aFalse aTrue).
contradiction (bFalse bTrue).
Qed.
Proof.
intros a b.
unfold not.
intros aFalse bFalse.
intros aORb.
destruct aORb as [aTrue | bTrue].
contradiction (aFalse aTrue).
contradiction (bFalse bTrue).
Qed.
Note: This shows a standard way to 'destruct' disjunctions in hypotheses:
Sort two cases: Left side of aORb (in our case it is aTrue).
The right side of aORb (in our case it is bTrue).
In both cases we get a contradiction.
Intuition: If 'a' and 'b' are not simultaneously true,
one of them implies the negation of another.
Lemma sample5: forall a b: Prop, ~(a /\ b) -> (b -> ~a).
Proof.
intros a b.
unfold not.
intros H.
intros bTrue.
intros aTrue.
apply H.
split.
exact aTrue.
exact bTrue.
Qed.
Proof.
intros a b.
unfold not.
intros H.
intros bTrue.
intros aTrue.
apply H.
split.
exact aTrue.
exact bTrue.
Qed.
Note: This shows a standard way to 'split' conjunction in the goal.
Split into two subgoals.
First prove the left part of the conjunction, then prove the right part.
Intuition: The tautology is a typical non-constructive stuff:
If '~b' implies '~a', and '~b' also implies 'a', then 'b' must be true
If '~b' implies '~a', and '~b' also implies 'a', then 'b' must be true
Lemma sample6: forall a b: Prop, (~b -> ~a) -> (~b -> a) -> b.
Proof.
intros a b.
unfold not.
intros H1.
intros H2.
pose (classic b) as H3.
destruct H3 as [bTrue | bFalse].
exact bTrue.
pose (H1 bFalse) as aFalse.
pose (H2 bFalse) as aTrue.
contradiction (aFalse aTrue).
Qed.
Proof.
intros a b.
unfold not.
intros H1.
intros H2.
pose (classic b) as H3.
destruct H3 as [bTrue | bFalse].
exact bTrue.
pose (H1 bFalse) as aFalse.
pose (H2 bFalse) as aTrue.
contradiction (aFalse aTrue).
Qed.
Note: Here is one new trick: First introduce 'classic' axiom;
then immediately destruct it into two subcases:
Intuition: Similar to the previous result:
If ~b implies ~a, and ~b also implies a,
then b must be true
- b=True. (Really easy case)
- b=False. In this situation we get contradictions with our earlier hypotheses.
Lemma sample7: forall a b: Prop, (a -> b) -> (~a -> b) -> b.
Proof.
intros a b.
intros H1.
intros H2.
pose (classic a) as H3.
destruct H3 as [aTrue | aFalse].
apply H1.
exact aTrue.
apply H2.
exact aFalse.
Qed.
Proof.
intros a b.
intros H1.
intros H2.
pose (classic a) as H3.
destruct H3 as [aTrue | aFalse].
apply H1.
exact aTrue.
apply H2.
exact aFalse.
Qed.
Note: Very similar to the previous case,
but it shows that you should pay attention to what
'classic' axiom you need. In this case we wanted to sort two cases:
Similar to sample6, but not exactly the same
- a = True
- b = False
Lemma sample8: forall a b: Prop, (a -> b) -> (a -> ~b) -> ~a.
Proof.
intros a b.
intros H1.
intros H2.
pose (classic a) as H3.
destruct H3 as [aTrue | aFalse].
contradiction ((H2 aTrue) (H1 aTrue)).
exact aFalse.
Qed.
Proof.
intros a b.
intros H1.
intros H2.
pose (classic a) as H3.
destruct H3 as [aTrue | aFalse].
contradiction ((H2 aTrue) (H1 aTrue)).
exact aFalse.
Qed.
Note: Pay attention to the latest long expression that gives contradiction.
Can rewrite the following expression:
contradiction ((H2 aTrue) (H1 aTrue)).as the following:
pose (H1 aTrue) as bTrue. pose (H2 aTrue) as bFalse. contradiciton (bFalse bTrue) as CONTRA.
Lemma sample9: forall a b: Prop, (~b -> a) -> (b -> a) -> a.
Proof.
intros a b.
unfold not.
intros H1.
intros H2.
pose (classic b) as H3.
destruct H3 as [bTrue | bFalse].
pose (H2 bTrue) as aTrue.
exact aTrue.
pose (H1 bFalse) as aTrue.
exact aTrue.
Qed.
Note: In the last few proofs there is a pattern:
Intution: If 'a','b' are either both True or both False, then ~a OR b must be True.
pose (classic b) as H3. destruct H3 as [bTrue | bFalse].In the following proof we show that you can rewrite this in a single line; and (instead of sorting two hypotheses) prove two separate goals.
Lemma sample10: forall a b: Prop, (a <-> b) -> (~a \/ b).
Proof.
intros a b.
intros H1.
destruct H1 as [H2 H3].
elim (classic a).
intros aTrue.
right.
apply (H2 aTrue).
intros aFalse.
left.
exact aFalse.
Qed.
Proof.
intros a b.
intros H1.
destruct H1 as [H2 H3].
elim (classic a).
intros aTrue.
right.
apply (H2 aTrue).
intros aFalse.
left.
exact aFalse.
Qed.
Intuition: If 'a','b' both together imply 'c'; and also 'a->b', then 'a->c'
Lemma sample11: forall a b c: Prop, (a -> b -> c) -> (a -> b) -> (a -> c).
Proof.
intros a b c H1 H2 aTrue.
apply (H1 aTrue).
apply (H2 aTrue).
Qed.
Proof.
intros a b c H1 H2 aTrue.
apply (H1 aTrue).
apply (H2 aTrue).
Qed.
Note: Some implications are easy, if they are constructive and
you can apply Modus Ponens - i.e. simply 'plug in' one expression into another
Intuition: 'a' implies 'b -> c' iff 'a and b' together imply 'c'
Lemma sample12: forall a b c: Prop, (a -> b -> c) <-> ((a /\ b) -> c).
Proof.
intros a b c.
split.
- intros H1.
intros [aTrue bTrue].
exact (H1 aTrue bTrue).
- intros H2.
intros aTrue bTrue.
assert (a /\ b) as H3.
split.
+ exact aTrue.
+ exact bTrue.
+ pose (H2 H3) as cTrue.
exact cTrue.
Qed.
Proof.
intros a b c.
split.
- intros H1.
intros [aTrue bTrue].
exact (H1 aTrue bTrue).
- intros H2.
intros aTrue bTrue.
assert (a /\ b) as H3.
split.
+ exact aTrue.
+ exact bTrue.
+ pose (H2 H3) as cTrue.
exact cTrue.
Qed.
Note: Tactic 'split' is useful when proving conjunctions and also equivalences.
In this case we need to check the statement in both directions.
Intuition: If both (a->c) and (b->c), and you know that (a \/ b) is True, then c is True
intros [aTrue bTrue].means the same as this:
intros myHypothesis. destruct myHypothesis as [aTrue bTrue].Preceding your subcases with '+' and '-' is sometimes used to split long proofs in shorter sections. It may keep things cleaner and more focused, but splitting into sections is never mandatory and does not affect the correctness of your proof.
Lemma sample13: forall a b c: Prop, (a -> c) -> (b -> c) -> (a \/ b) -> c.
Proof.
intros a b c.
intros H1.
intros H2.
intros [aTrue | bTrue].
exact (H1 aTrue).
exact (H2 bTrue).
Qed.
Proof.
intros a b c.
intros H1.
intros H2.
intros [aTrue | bTrue].
exact (H1 aTrue).
exact (H2 bTrue).
Qed.
Note: One more shorthand notation:
Intuition: Just a statement that if (a->b) and (c->a), then (c->b).
Transitivity - similar to the problem in Homeowork 2, Q2.C.
It was about the plane/railway traffic being transitive.
intros [aTrue | bTrue].is same as this:
intros H. destruct H as [aTrue | bTrue].
Lemma sample14: forall a b c: Prop, (a -> b) -> (c -> a) -> (c -> b).
Proof.
intros a b c.
intros H1 H2 cTrue.
exact (H1 (H2 cTrue)).
Qed.
Proof.
intros a b c.
intros H1 H2 cTrue.
exact (H1 (H2 cTrue)).
Qed.
Intuition: Some variant to say that disjunction is associative; and one can regroup.
Lemma sample15: forall a b c: Prop, a \/ (b \/ c) -> (b \/ (a \/ c)) \/ a.
Proof.
intros a b c.
intros [H2 | H3].
right; exact H2.
destruct H3 as [H4 | H5].
left; left; exact H4.
left; right; right; exact H5.
Qed.
Proof.
intros a b c.
intros [H2 | H3].
right; exact H2.
destruct H3 as [H4 | H5].
left; left; exact H4.
left; right; right; exact H5.
Qed.
The long expression with semicolons (;)
left; right; right; exact H5.
applies all the goals right after one another (one big jump).
How to expalain this? We have the following goal:
'left' on '(b \/ (a \/ c)) \/ a' is '(b \/ (a \/ c))'
'right' on '(b \/ (a \/ c))' is '(a \/ c)'.
'right' on '(a \/ c)' is 'c'.
It is exactly our hypothesis H5.
Intuition: Realy easy lemma: If 'a' and then 'b' both imply 'c',
then 'b' and 'a' (switched places) imply 'c'
(b \/ a \/ c) \/ a.It seems that disjunction is right-associative:
(b \/ a \/ c) \/ a = (b \/ (a \/ c)) \/ a.Our hypothesis H5 says that 'c' must be True. We can 'drill down' to that variable:
'left' on '(b \/ (a \/ c)) \/ a' is '(b \/ (a \/ c))'
'right' on '(b \/ (a \/ c))' is '(a \/ c)'.
'right' on '(a \/ c)' is 'c'.
It is exactly our hypothesis H5.
Lemma sample16: forall a b c: Prop, (a -> (b -> c)) -> (b -> (a -> c)).
Proof.
intros a b c.
intros H bTrue aTrue.
exact ((H aTrue) bTrue).
Qed.
Proof.
intros a b c.
intros H bTrue aTrue.
exact ((H aTrue) bTrue).
Qed.
Note: Here we pass two arguments to the 'two-argument' hypothesis H.
The notation:
Intuition: Implication is transitive'; similar to 'sample14', but switched order.
(H aTrue bTrue)actually means this: ((H aTrue) bTrue). It is not same as:
(H (aTrue bTrue))Function/implication application is left-associative.
Lemma sample17: forall a b c: Prop, (a -> b) -> (b -> c) -> (a -> c).
Proof.
intros a b c H1 H2 aTrue.
exact (H2 (H1 aTrue)).
Qed.
Proof.
intros a b c H1 H2 aTrue.
exact (H2 (H1 aTrue)).
Qed.
Note:
In this case we need to group the function application from right to left
Intuition: If (a and b) imply c, then 'a' implies that 'b' implies 'c'
Lemma sample18: forall a b c: Prop, ((a /\ b) -> c) -> (a -> (b -> c)).
Proof.
intros a b c.
intros H1 aTrue bTrue.
assert (a /\ b) as aANDb.
split.
exact aTrue.
exact bTrue.
exact (H1 aANDb).
Qed.
Proof.
intros a b c.
intros H1 aTrue bTrue.
assert (a /\ b) as aANDb.
split.
exact aTrue.
exact bTrue.
exact (H1 aANDb).
Qed.
Intuition: 'a' implies 'b and c' iff 'a->b' and 'a->c'
Lemma sample19: forall a b c: Prop, (a -> b /\ c) <-> (a -> b) /\ (a -> c).
Proof.
intros a b c.
split.
- intros H1.
split.
+ intros aTrue.
destruct (H1 aTrue) as [bTrue _].
exact bTrue.
+ intros aTrue.
destruct (H1 aTrue) as [_ cTrue].
exact cTrue.
- intros [H2 H3].
intros aTrue.
split.
+ exact (H2 aTrue).
+ exact (H3 aTrue).
Qed.
Proof.
intros a b c.
split.
- intros H1.
split.
+ intros aTrue.
destruct (H1 aTrue) as [bTrue _].
exact bTrue.
+ intros aTrue.
destruct (H1 aTrue) as [_ cTrue].
exact cTrue.
- intros [H2 H3].
intros aTrue.
split.
+ exact (H2 aTrue).
+ exact (H3 aTrue).
Qed.
Intuition: The final 2 lemmas are not too intuitive, but they are also tautologies.
Once again a long proof structured into subsections.
Once again a long proof structured into subsections.
Lemma sample20: forall a b c d e: Prop,
((((a -> b) -> (~c -> ~d)) -> c) -> e) -> ~a -> (d -> e).
Proof.
intros a b c d e.
intros H1.
intros aFalse.
intros dTrue.
assert (((a -> b) -> ~ c -> ~ d) -> c) as H4.
intros H5.
assert (a -> b) as H6.
intros aTrue.
contradiction (aFalse aTrue).
pose (H5 H6) as H7.
apply NNPP.
unfold not.
intros cFalse.
contradiction ((H7 cFalse) dTrue).
exact (H1 H4).
Qed.
Corollary longTautology: forall a b c d e: Prop,
((((a -> b) -> (~c -> ~d)) -> c) -> e) -> ((e -> a) -> (d -> a)).
Proof.
intros a b c d e.
intros H1 H2 dTrue.
destruct (classic a) as [aTrue | aFalse].
exact aTrue.
pose (sample20 a b c d e) as H3.
pose (H3 H1) as H4.
pose (H4 aFalse) as H5.
pose (H5 dTrue) as eTrue.
pose (H2 eTrue) as aTrue.
exact aTrue.
Qed.
((((a -> b) -> (~c -> ~d)) -> c) -> e) -> ~a -> (d -> e).
Proof.
intros a b c d e.
intros H1.
intros aFalse.
intros dTrue.
assert (((a -> b) -> ~ c -> ~ d) -> c) as H4.
intros H5.
assert (a -> b) as H6.
intros aTrue.
contradiction (aFalse aTrue).
pose (H5 H6) as H7.
apply NNPP.
unfold not.
intros cFalse.
contradiction ((H7 cFalse) dTrue).
exact (H1 H4).
Qed.
Corollary longTautology: forall a b c d e: Prop,
((((a -> b) -> (~c -> ~d)) -> c) -> e) -> ((e -> a) -> (d -> a)).
Proof.
intros a b c d e.
intros H1 H2 dTrue.
destruct (classic a) as [aTrue | aFalse].
exact aTrue.
pose (sample20 a b c d e) as H3.
pose (H3 H1) as H4.
pose (H4 aFalse) as H5.
pose (H5 dTrue) as eTrue.
pose (H2 eTrue) as aTrue.
exact aTrue.
Qed.