Commit 878be73d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

demo1 for proof mode and basic connectors

parent c363e5a3
(* A first universe seen earlier : Type
(and Set is Type(0). *)
Check 0.
Check nat.
Check Set. (* Alias for the first level Type(0) *)
Check Type.
(* Another universe : Prop
The universe of logical statement and proofs *)
(* For proofs *)
Check I. (* is the canonical proof of True, hence I : True *)
Check True.
Check Prop.
(*
Type(..)
|
Type(1)
/ \
Set=Type(0) Prop
| | \
nat True False
| |
O I - (no close proof of False)
*)
(* A statement is something of type Prop *)
(* A proof is an inhabitant of a statement *)
Lemma my_first_proof : True.
Proof.
exact I.
Qed.
Print my_first_proof.
(* Just about the same as this:
Definition my_first_proof_bis : True := I.
*)
(* Operators, for building more advanced statements *)
(* Arrow -> *)
Check nat -> nat.
Check True -> True.
Lemma proof2 : True -> True.
Proof.
exact (fun _ => I).
Qed.
(* or step by step : *)
(* intro : the tactic of introduction of -> : *)
(* A |- B *)
(* |- A->B *)
Lemma proof3 : True -> True.
Proof.
intro.
Show Proof. (* to inspect the proof term being built *)
assumption. (* the "axiom rule" of natural deduction *)
Qed.
Print proof3.
(* forall : the dependent version of the ->
same introduction tactic : intro. *)
Lemma identity : forall (A:Prop), A -> A.
Proof.
intros A a.
assumption.
Qed.
Print identity.
(* forall and its non-dependent version -> are the
only primitive operators.
introduction : intro / intros / intros ...
elimination : apply H.
*)
Lemma test : forall (A B : Prop), (A->B)->A->B.
Proof.
intros A B f a.
apply f.
(* assumption. *) (*apply a.*) exact a.
Qed.
Print test.
Lemma test' : forall (A B : Prop), (A->B)->A->B.
Proof.
auto.
Qed.
(* Other operators *)
(* I : True *)
Check False. (* no closed construction *)
Lemma efql : False -> forall (A:Prop), A.
Proof.
intro fa.
intro A.
destruct fa. (* elimination of a False hypothesis *)
Qed.
(* negation is a shortcut for ...->False *)
Check ~True.
Check True -> False.
(*
Lemma attempt : ~True.
Proof.
unfold "~" in *. (* not a mandatory step *)
intro.
*)
(* /\ and : introduction via split
elimination via destruct ... *)
Parameter A B : Prop.
Lemma conj : A/\B -> B/\A.
Proof.
intro.
destruct H.
split.
- assumption.
- assumption.
Qed.
(* Available bullets for structuring a proof script : - + *
*)
(* \/ or : introduction via : left / right
elimination via destruct ...*)
Lemma disj : A\/B -> B\/A.
Proof.
intro.
destruct H.
- right. assumption.
- left. assumption.
Qed.
(* exists : introduction via : exists ...
elimination via : destruct ...
*)
Lemma example_exists : exists x : nat, x = 0.
Proof.
exists 0. reflexivity.
Qed.
(* A<->B its a shortcut for (A->B)/\(B->A) *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment