Proofs in Proposition Logic and Predicate Logic

Proofs in Proposition Logic and Predicate Logic

1
Pierre Casteran
Beijing, August 2009
1
This lecture corresponds mainly to the chapters 3 : Propositions and
Proofsand 5 : Everyday Logicof the book.
Proofs in Proposition Logic and Predicate Logic
In this class, we introduce the reasoning techniques used in Coq,
starting with a very reduced fragment of logic, propositional
intuitonistic logic, then rst-order intuitonistic logic.
We shall present :

The logical formulas and the statements we want to prove,

How to build proofs interactively.

Proofs in Proposition Logic and Predicate Logic
Propositions and Types
The Type Prop
In Coq, a predened type, namely Prop, is inhabited by all logical
propositions. For instance the true and false propositions are simply
constants of type Prop :
Check True.
True : Prop
Check False.
False : Prop
Dont mistake the proposition True (resp. False) for the boolean
true (resp. false), which belong to the bool datatype.
Proofs in Proposition Logic and Predicate Logic
Propositions and Types
Since Prop is a type, it is easy to declare propositional variables,
using Coqs declaration mechanism :
Section Propositional_Logic.
Variables P Q R T : Prop.
P is assumed
2
Q is assumed . . .
Check P.
P : Prop
2
read P is assumed to be a proposition
Proofs in Proposition Logic and Predicate Logic
Propositions and Types
Propositional Formulas
One can build propositions by using the following rules :

Each variable of type Prop is a proposition,

The constants True and False are propositions,

if A and B are propositions, so are :

A B (logical equivalence) (in ASCII : A <-> B)

A B (implication) (in ASCII : A -> B)

A B (disjunction) (in ASCII : A \/ B )

A B (conjunction) (in ASCII : A /\ B)

A (negation)
Check ((P (Q P)) (Q P)).
(P Q P) Q P : Prop
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
The Sequent Notation
In Coq, a frequent activity consists in proving a proposition A
under some set of hypotheses (also called a context.)
For instance, one would like to prove the formula R P under the
hypotheses R P Q and (R Q).
A structure consisting of a nite set of hypotheses and a
conclusion A is called an (intuitonistic) sequent. Its usual notation
is A.
In our example, the sequent we consider is written :
RPQ, (RQ)

hypotheses
RP

conclusion
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
Hypotheses and Goals
The Coq system helps the user to build interactively a proof of
some sequent A. We also say that one wants to solve the goal

?
A.
In Coq a goal is shown as below : each hypothesis is given a
distinct name, and the conclusion is displayed under a bar which
separates it from the hypotheses :
H : R P Q
H0 : (R Q)
============================
R P
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
In the proof of some theorem, it is usual to have to prove several
subgoals. In this case, Coq displays in full the rst subgoal to solve,
and an abbreviated view of the remaining subgoals.
2 subgoals
P : Prop
Q : Prop
H : P Q
H0 : P
============================
Q P
subgoal 2 is:
Q P
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
Rules and Tactics
Let us consider some goal
?
A. Solving this goal consists in
building a proof of A under the hypotheses of . Formally, such a
proof is a term of type A, but we wont explore deeply this aspect
(see the book for more details).
The structure of a proof both depends on the form of A and the
contents of . We will present now some basic rules for building
proofs.
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
Goal Directed Proofs
Tactic application can be slightly more complex in some situations
(e.g. shared existential variables, see Coqs documentation).
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
More details
The basic tool for interactively solving a goal G =
?
A is called a
tactic, which is a command typed by the user.
In general, at each step of an interactive proof, a nite sequence of
subgoals G
1
, G
2
, . . . , G
n
must be solved. An elementary step of an
interactive proof has the following form : The user tries to apply a
tactic to (by default) the rst subgoal G
1
,

This application may fail, in which case the state of the proof
doesnt change,

or this application generates a nite sequence (possibly

empty) of new subgoals, which replace the previous one.
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
When is an interactive proof nished ?
The number of subgoals that remain to be solved decreases only
when some tactic application generates 0 new subgoals.
The interactive search of a proof is nished when there remain no
subgoals to solve. The Qed command makes Coq do the following
actions :
1. build a proof term from the history of tactic invocations,
2. check whether this proof is correct,
3. register the proven theorem.
Proofs in Proposition Logic and Predicate Logic
Sequents and Goals
Introduction and Elimination Tactics
Let us consider again the goal below :
H : R P Q
H0 : (R Q)
============================
R P
We colored in blue the main connective of the conclusion, and in
red the main connective of each hypothesis.
To solve this goal, we can use an introduction tactic associated to
the main connective of the conclusion, or an elimination tactic on
some hypothesis.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
Minimal Propositional Logic
Minimal propositional logic is a very simple fragment of
mathematical logic :

Formulas are built only with propositional variables and the

implication connective .

There are only three simple inference rules.

It is a good framework for learning basic concepts on tactics in
Coq.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
The rule of assumption
The following rule builds a proof of any sequent A, whenever
the conclusion A is already assumed in .
A
A
assumption
In an interactive proof with Coq, the tactic assumption solves any
goal
?
A, where the context contains an hypothesis assuming A.
H : R P Q
H0 :(R Q) T
============================
R P Q
assumption.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
Elimination rule for the implication (modus ponens)
. . .
BA
. . .
B
A
mp
Applying several times the mp rule, we get the following derived
rule :
. . .
A
1
A
2
. . . A
n
A
. . .
A
1
. . .
A
2
. . .
. . .
A
n
A
Let us consider a goal of the form
?
A. If H : A
1
A
2
. . . A
n
A
is an hypothesis of or an already proven theorem, then the tactic
apply H generates n new subgoals,
?
A
1
, . . .,
?
A
n
.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
Introduction rule for the implication
. . .
, A B
AB
imp i
Let us consider a goal
?
AB. The tactic intro H (where H is
not the name of an hypothesis in ) transforms this goal into
, H : A
?
B.
The multiple introduction tactic intros H1 H2 . . .Hn is a shortand
for intro H1 ; intro H2 ; . . . ; intro Hn.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
A simple example
The following proof tree represents a proof of the sequent
(PQR)(PQ)(PR). The leaves of this tree are
instances of rule assumption. For simplicitys sake, we use as an
abbreviation of the context PQR, PQ.
, P PQR , P P
, P QR
mp
, P PQ , P P
, P Q
mp
, P R
mp
PR
imp i
PQR (PQ)(PR)
imp i
(PQR)(PQ)(PR)
imp i
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
The same proof using tactics
Section Propositional_Logic.
Variables P Q R : Prop.
Lemma imp_dist : (P (Q R)) (P Q) P R.
Proof.
1 subgoal
P : Prop
Q : Prop
R : Prop
============================
(P Q R) (P Q) P R
intros H H0 p.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
1 subgoal:
P : Prop
Q : Prop
R : Prop
H : P Q R
H0 : P Q
p : P
============================
R
apply H.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
2 subgoals:
P : Prop
Q : Prop
R : Prop
H : P Q R
H0 : P Q
p : P
============================
P
subgoal 2 is:
Q
assumption.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
1 subgoal:
P : Prop
Q : Prop
R : Prop
T : Prop
H : P Q R
H0 : P Q
p : P
============================
Q
apply H0;assumption.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
Proof completed
Qed.
imp dist is dened
Check imp_dist.
imp dist
: (P Q R) (P Q) P R
Print imp_dist.
imp dist =
fun (H : P Q R) (H0 : P Q) (H1 : P) H H1 (H0 H1)
: (P Q R) (P Q) P R
We notice that the internal representation of the proof we have
just built is a term whose type is the theorem statement.
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
It is possible, but not usual, to build directly proof terms,
considering that a proof of AB is just a function which maps any
proof of A to a proof of B.
Check fun p:P p.
fun p:P p
: P P
Check fun (H : P Q R)(q: Q)(p:P) H p q.
fun (H : P Q R) (q : Q) (p : P) H p q
: (P Q R) Q P R
Check fun (p:P)(H: P False) H p.
fun (p : P) (H : P False) H p
: P (P False) False
Proofs in Proposition Logic and Predicate Logic
Minimal Propositional Logic
Using the section mechanism
Another way to prove an implication AB is to prove B inside a
section which contains a hypothesis assuming A, if the proof of B
uses truely the hypothesis assuming A. This scheme generalizes to
any number of hypotheses A
1
, . . . , A
n
.
Section Imp_trans.
Hypothesis H : P Q.
Hypothesis H0 : Q R.
Lemma imp_trans: P R.
(* Proof skipped, uses H and H0 *)
End Imp_trans.
Check imp_trans.
imp trans : (P Q) (Q R) P R
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Propositional Intuitionistic Logic
We will now add to Minimal Propositional Logic introduction and
elimination rules and tactics for the constants True and False, and
the connectives and (), or (), i () and not ().
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Introduction rule for True
In any context the proposition True is immediately provable
(thanks to a predeclared constant I :True).
Practically, any goal
?
True can be solved by the tactic trivial :
H : R P Q
H0 : (R Q)
============================
True
trivial.
There is no useful elimination rule for True.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Falsity
The elimination rule for the constant False implements the
so-called principle of explosion, according to whichany proposition
follows from a contradiction.
False
A
False e
There is an elimination tactic for False : Let us consider a goal of
the form
?
A , and an hypothesis H :False. Then the tactic
destruct H solves this goal immediately.
In order to avoid to prove contradictions, there is no introduction
rule nor introduction tactic for False.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Introduction rule and tactic for conjunction
A proof of a sequent AB is composed of a proof of A
and a proof of B.
. . .
A
. . .
B
AB
conj
Coqs tactic split, splits a goal
?
AB into two subgoals
?
A
and
?
B.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Conjunction elimination
Rule :
. . .
AB
. . .
, A, B C
C
and e
Associated tactic :
Let us consider a goal
?
C, and H :AB. Then the tactic
destruct H as [H1 H2] generates the new goal
, H1 : A, H2 : B
?
C
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Example
Lemma and_comm : P Q Q P.
Proof.
intro H.
1 subgoal
P : Prop
Q : Prop
H : P Q
============================
Q P
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
destruct H as [H1 H2].
1 subgoal
P : Prop
Q : Prop
H1 : P
H2 : Q
============================
Q P
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
split.
2 subgoals
P : Prop
Q : Prop
H1 : P
H2 : Q
============================
Q
subgoal 2 is:
P
...
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Introduction rules and tactics for disjunction
There are two introduction rules for :
. . .
A
AB
or intro l
. . .
B
AB
or intro r
The tactic left is associated to or intro l, and the tactic right to
or intro r.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Elimination rule and tactic for disjunction
. . .
AB
. . .
, A C
. . .
, B C
C
or e
Let us consider a goal
?
C, and H :AB. Then the tactic
destruct H as [H1 | H2] generates two new subgoals :
, H1 : A
?
C
, H2 : B
?
C
This tactic implements the proof by cases paradigm.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
A combination of left, right and destruct
Consider the following goal :
P : Prop
Q : Prop
H : P Q
============================
Q P
We have to choose between an introduction tactic on the
conclusion Q P, or an elimination tactic on the hypothesis H.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
If we start with an introduction tactic, we have to choose between
left and right. Let us use left for instance :
left.
P : Prop
Q : Prop
H : P Q
============================
P
This is clearly a dead end. Let us come back to the previous step
(with command Undo).
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
destruct H as [H0 | H0].
two subgoals
P : Prop
Q : Prop
H : P Q
H0 : P
============================
Q P
subgoal 2 is :
Q P
right;assumption.
left;assumption.
Qed.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Negation
In Coq, the negation of a proposition A is represented with the
help of a constant not, where not A (also written A) is dened as
the implication AFalse.
The tactic unfold not allows to expand the constant not in a goal,
but is seldom used.
The introduction tactic for A is the introduction tactic for
AFalse, i.e. intro H where H is a fresh name. This tactic pushes
the hypothesis H : A into the context and leaves False as the
proposition to prove.
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Elimination tactic for the negation
The elimination tactic for negation implements some kind of
reasoning by contradiction (absurd).
Let us consider a goal , H : B
?
A. Then the tactic destruct H
generates a new subgoal
?
B.
Justication (by a derived rule) :
. . .
B
, H : B B
, H : B B
, H : B BFalse
, H : B False
, H : B A
Proofs in Proposition Logic and Predicate Logic
Propositional Intuitionistic Logic
Logical equivalence
Let A and B be two propositions. Then the formula A B (read
A i B) is dened as the conjunction (AB)(AB).
The introduction tactic for is split, which associates to any goal

?
A B tho subgoals
?
AB and
?
BA.
The elimination tactic for is destruct H as [H1 H2] where H is
an hypothesis of type A B and H1 and H2 arefreshnames.
This tactic adds to the current context the hypotheses H1 : A B
and H2 : B A.
Proofs in Proposition Logic and Predicate Logic
More on tactics
Simple tactic composition
Let tac and tac be two tactics.
The tactic tac ;tac applies tac to each subgoal generated by the
application of tac to the rst subgoal.
Proofs in Proposition Logic and Predicate Logic
More on tactics
Lemma and_comm : P Q Q P.
Proof.
intro H;destruct H as [H1 H2].
H1 : P
H2 : Q
============================
Q P
split;assumption.
(* assumption has been applied to each one of the
two subgoals generated by split *)
Qed.
Proofs in Proposition Logic and Predicate Logic
More on tactics
Another composition operator
The tactic composition tac ;[tac1|tac2|. . .] is a generalization of the
simple composition operator, in situations where the same tactic
cannot be applied to each generated new subgoal.
Proofs in Proposition Logic and Predicate Logic
More on tactics
The assert tactic (forward chaining)
Let us consider some goal
?
A, and B be some proposition.
The tactic assert (H :B), generates two subgoals :
1.
?
B
2. , H : B
?
A
This tactic can be useful for avoiding proof duplication inside some
interactive proof. Notice that the scope of the declaration H :B is
limited to the second subgoal. If a proof of B is needed elsewhere,
it would be better to prove a lemma stating B.
Remark : Sometimes the overuse of assert may lead to verbose
developments (remember that the user has to type the statement
B !)
Proofs in Proposition Logic and Predicate Logic
More on tactics
Section assert.
Hypotheses (H : P Q)
(H0 : Q R)
(H1 : (P R) T Q)
(H2 : (P R) T).
Lemma L8 : Q.
(* A direct backward proof would need to prove twice
the proposition (P R) *)
The tactic assert (PR : P R) generates two subgoals :
Proofs in Proposition Logic and Predicate Logic
More on tactics
2 subgoals
H : P Q
H0 : Q R
H1 : (P R) T Q
H2 : (P R) T
============================
P R
Q
intro p;apply H0;apply H;assumption.
Proofs in Proposition Logic and Predicate Logic
More on tactics
H : P Q
H0 : Q R
H1 : (P R) T Q
H2 : (P R) T
PR : P R
============================
Q
apply H1; [ assumption | apply H2;assumption].
Qed.
Proofs in Proposition Logic and Predicate Logic
More on tactics
A more clever use of destruct
The tactic destruct H works also when H is an hypothesis (or
axiom , or already proven theorem), of type A
1
A
2
. . . A
n
A
where the main connective of A is , , , or False.
In this case, new subgoals of the form
?
A
i
are also generated (in
addition to the behaviour we have already seen).
In fact, this use of destruct H replaces a composition of calls to
assert, applications, and destruct. Notice the use of H as a
function that receives as arguments proofs of A
1
, A
2
, . . . , A
n
.
assert (H1:A1);[auto |
assert(H2:A2);[auto|
...
assert (Hn:An);[auto |
destruct (H H1 H2 ... Hn)]]]
Proofs in Proposition Logic and Predicate Logic
More on tactics
Section Ex5.
Hypothesis H : T R P Q.
Hypothesis H0 : (R Q).
Hypothesis H1 : T.
Lemma L5 : R P.
Proof.
intro r.
Destructuring H will produce four subgoals :

prove T

prove R

assuming P, prove P,

assuming Q, prove P.
Proofs in Proposition Logic and Predicate Logic
More on tactics
(* Let us try to apply assumption
to each of these four subgoals *)
destruct H as [H2 | H2] ;try assumption.
1 subgoal
H : T R P Q
H0 : (R Q)
H1 : T
r : R
H2 : Q
============================
P
destruct H0; split;assumption.
Qed.
Proofs in Proposition Logic and Predicate Logic
More on tactics
An automatic tactic for intuitionistic propositional logic
The tactic tauto solves goals which are instances of intuitionnistic
propositional tautologies.
Lemma L5 : (R P Q) (R Q) R P.
Proof.
tauto.
Qed.
The tactic tauto doesnt solve goals that are only provable in
classical propositional logic (i.e. intuitionnistic + the rule of
excluded middle AA). Here are some examples :
P P
(P Q) ( P Q)
(P Q) P Q
((P Q) P) P (Peirces formula)
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Formulas of First-Order Logic : 1

Terms : we can build terms according to the declarations of

constants and variables, using Coqs typing rules.

Predicates : a Predicate is just any function of type

A
1
A
2
. . . A
n
Prop where A
i
: Set for each i . Predicates are
declared as any other function symbol.

Atomic propositions : let P : A

1
A
2
. . . A
n
Prop and
t
i
: A
i
(i = 1 . . . n). Then the term f t
1
t
2
. . . t
n
of sort Prop
is an atomic proposition.
If t
1
and t
2
are terms of the same type, then t
1
= t
2
is an
atomic proposition.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
First Order formulas : 2
According to the declarations of the current context :

Any atomic formula is a formula,

True and False are formulas,

If F and G are formulas, then FG, FG, FG, FG and

F are formulas,

let x be a variable, then x:A, F and x : A, F are formulas.

x is said to be bound in F.
ASCII notation : The symbol is typed forall and is typed exists.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Examples
Section First_Order.
Variable A : Type.
Variable R : A A Prop.
Variable f : A A.
Variable a : A.
Check f (f a).
(f (f a)) : A
Check R a (f (f a)).
R a (f (f a)): Prop
Check forall x :A, R a x R a (f (f (f x))).
forall x :A, R a x R a (f (f (f x))) : Prop.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Introduction rule for the universal quantier
, x : A F
x:A, F
x not bound in
The tactic associated with this rule is the same as for the
introduction of implication : intro x.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
It is very usual to use intros on nested universal quantications and
implications :
. . .
===================
forall x :A, P x forall y: A, R x y R x (f (f (f y))).
intros x Hx y Hy.
. . .
x: A
Hx: P x
y: A
H: R x y
======================
R x (f (f (f y)))
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Elimination rule for the universal quantier
t : A
. . .
x:A, F
F{x/t}

e
The associated tactic is apply H, where H has type x:A, F . This
tactic is generalized to the case of nested implications and
universal quantications, like, for instance :
H : x:A, P x y:A, R x y R x (f y)
On a goal like R a (f (f a)), the tactic apply H will generate two
subgoals : P a and R a (f a).
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
A Small Example
Hypothesis Hf : forall x y:A, R x y R x (f y).
Hypothesis R_refl : forall x:A, R x x.
Lemma Lf : forall x :A, R x (f (f (f x))).
Proof.
intro x;apply Hf.
1 subgoal
Hf : forall x y : A, R x y R x (f y)
R re : forall x : A, R x x
x : A
============================
R x (f (f x))
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Helping apply
Let us use the following theorems from the library Arith :
lt n Sn : forall n : nat, n < S n
lt_trans : forall n m p : nat, n < m m < p n < p
Lemma lt_n_SSn : forall i:nat, i < S (S i).
Proof.
intro i;apply lt_trans.
Error: Unable to nd an instance for the variable m.
intro i;apply lt_trans with (S i);apply lt_n_Sn.
Another possibility : use eapply (see the documentation).
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Introduction rule for the existential quantier
F{x/t} t : A
x : A, F

i
The associated tactic is exists t.
========
exists p, 3 < p.
exists 4.
==============
3 < 4
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Elimination rule for the existential quantier
. . .
, x : A, Hx : F G x : A, F
G
x not bound in
The associated tactic is destruct H as [x Hx], where H :x : A, F
w.r.t. .
H : exists n:nat, forall p: nat, p < n
===================
False
destruct H as [n Hn].
n : nat
Hn : forall p : nat, p < n
============================
False
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Rules and tactics for the equality
Introduction rule.
a : A
a = a
re equal
Associated tactics : reexivity, trivial, auto.
Lemma L36 : 9 * 4 = 3 * 12.
Proof.
reflexivity.
Qed.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Elimination tactics for the equality
, e : a = b A[a]
, e : a = b A[b]
The associated tactic is rewrite e.
, e : a = b A[b]
, e : a = b A[a]
The associated tactic is rewrite e.
See also : tactics symmetry, transitivity, replace, etc.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Example
Lemma eq_trans_on_A :
forall x y z:A, x = y y = z x = z.
Proof.
intros x y z e.
. . .
e : x = y
============================
y = z x = z
rewrite e.
. . .
e : x = y
============================
y = z y = z
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Autres tactiques pour legalite

symmetry transforme un but t

1
= t
2
en t
2
= t
1

transitivity t
3
transforme un but t
1
= t
3
en les deux sous-buts
t
2
= t
3
et t
3
= t
2
Voir aussi replace, subst, etc.
Proofs in Proposition Logic and Predicate Logic
First Order Intuitionistic Logic
Utilisation de lapplication
Require Import Omega.
Lemma L : forall n:nat, n < 2 -> n = 0 n = 1.
Proof.
intros;omega.
Qed.
Lemma L2 : forall i:nat, i < 2 -> i*i = i.
Proof.
intros i H; destruct (L _ H); subst i; trivial.
Qed.