Library logic_example
Module minimal_Gallina_introduction.
Variable x : Prop.
Variables A B : Prop.
Variable t2 : Prop.
Check A -> B : Prop.
Check (fun y => y -> y) : Prop -> Prop.
Definition t1_oops := fun y => y -> y.
Check t1_oops.
Definition t1 := fun y : Prop => y -> y.
Check t1.
Check (t1 t2) : Prop.
Check (Prop -> Prop) -> B.
Fail Check (fun y : Prop => y -> y) -> B.
End minimal_Gallina_introduction.
From Ssreflect Require Import ssreflect.
Module propositions_as_types_example.
Lemma hilbertS (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
Show Proof.
move=> H1.
Show Proof. move=> H2.
move=> H3.
Show Proof.
cut B. Show Proof.
cut A.
Show Proof.
assumption.
assumption.
Show Proof.
cut A.
assumption.
assumption.
Show Proof.
Qed.
Definition hilbertS_proof :=
fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
(fun H : B => (fun H0 : A => H1 H0) H3 H) ((fun H : A => H2 H) H3).
Lemma hilbertS_direct_proof (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
exact (hilbertS_proof A B C).
Qed.
Lemma hilbertS_in_practice (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
move=> H1.
move=> H2.
move=> H3.
apply H1.
exact H3.
apply H2.
exact H3.
Show Proof.
Qed.
Definition hilbertS_in_practice_proof :=
fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
H1 H3 (H2 H3).
Goal hilbertS_proof = hilbertS_in_practice_proof.
reflexivity.
Qed.
End propositions_as_types_example.
Module move_and_apply_tactics.
Lemma modus_ponens : forall P Q : Prop, (P -> Q) -> P -> Q.
Show Proof.
move=> P.
move: P.
move=> P Q PQ p.
move: PQ.
apply.
done.
Qed.
Goal forall P Q : Prop, (forall R : Prop, R -> Q) -> P -> Q.
Proof.
move=> P Q rq p.
Fail apply rq.
apply: rq p.
Qed.
Variable A : Prop.
Variable op : A -> A -> A.
Local Notation "a + b" := (op a b). Hypothesis opA : forall a b c, a + (b + c) = a + b + c.
Check opA.
Variable lt : A -> A -> Prop.
Local Notation "a < b" := (lt a b).
Hypothesis lt_addr : forall m n p, m < n -> m < n + p.
Goal forall a b c d,
a < b ->
a < b + c + d.
move=> a b c d.
Fail apply lt_addr.
rewrite -opA.
apply lt_addr.
Qed.
Goal False.
evar (x : nat).
have : (2 + x = 4 + 5)%nat.
rewrite /x.
apply refl_equal.
rewrite /= in x *.
Abort.
End move_and_apply_tactics.
Lemma exo0 : forall P : Prop, P -> P.
Proof.
Admitted.
Lemma exo1 : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
Admitted.
Lemma exo2 : forall P : Prop, (P -> P) -> P -> P.
Proof.
Admitted.
Lemma exo3 P Q R : (P -> Q) -> (Q -> R) -> P -> R.
Proof.
Admitted.
Section logical_connectives.
Print True.
Check True.
Check I.
Goal True.
apply: I.
Qed.
Print False.
Goal True -> False.
case.
Show Proof.
Abort.
Check False_ind.
Goal False -> 1 = 0.
move=> p.
exact: (False_ind (1 = 0) p).
Qed.
Goal False -> 1 = 0.
case.
Qed.
Print and.
Check conj I I.
Print and_ind.
Print and_rect.
Goal forall P Q, P /\ Q -> Q /\ P.
move=> P Q.
case.
Show Proof.
move=> p q.
split.
exact q.
exact p.
Qed.
Print or.
Check or_ind.
Check (or_intror False I).
About or_intror.
Check (@or_intror False True I).
Check (@or_intror False _ I).
Check (@or_intror _ _ I).
Check (@or_intror _ _ I) : False \/ True.
Goal forall A B, A \/ B -> B \/ A.
move=> A B.
case => [a | b].
right.
exact.
left.
exact b.
Qed.
End logical_connectives.
Lemma exo4 : False \/ True.
Proof.
Abort.
Lemma exo5 : forall A B C : Prop, A /\ B <-> B /\ A.
Proof.
move=> A B C.
Locate "<->".
Print iff.
Abort.
Lemma exo6 (A B C : Prop) : A /\ B /\ C ->
(A /\ B) /\ C.
Proof.
Abort.
Lemma exo7 (A B : Prop) : (A -> B) -> (~B -> ~A).
Proof.
Abort.
Section Set_Prop.
Check nat.
Goal 0 = 1 -> False.
move=> abs.
discriminate.
Qed.
Goal (exists n : nat, True) -> nat.
Fail case.
Abort.
About ex.
Goal forall A B : Prop, A \/ B -> nat.
move=> A B.
Fail case.
Abort.
Goal 0 = 1 -> nat.
move=> abs.
discriminate.
Show Proof.
Qed.
Goal forall n m : nat, n = m /\ n <> m -> nat.
move=> n m.
case => nm nm'.
exact O.
Qed.
Print sum.
Print sumbool.
Print sumor.
About sig.
Goal {n : nat | True} -> nat.
case.
move=> m _.
exact m.
Qed.
End Set_Prop.
Section product_formation.
Check Prop.
Check Set.
Set Printing Universes.
Check Type.
Unset Printing Universes.
Variables P0 P1 : Prop.
Check P0 -> P1 : Set.
Check P0 : Set.
Check P0 : Type.
Variable S0 : Set.
Check S0 : Type.
Check P1 -> P1 : Prop.
Check (S0 -> P0) : Prop.
Variable T0 : Type.
Check (T0 -> P0) : Prop.
Check (True -> True).
Check (forall x : nat, 0 <= x).
Check (forall x : nat, x = x) : Set.
Check (forall A : Prop, A -> A).
Check nat -> Prop.
Check (forall P : nat -> Prop, P O -> exists n : nat , P n) : Prop.
Check (P0 -> S0) : Set.
Fail Check (P0 -> S0) : Prop.
Variable S1 : Set.
Check (S1 -> S0) : Set.
Fail Check (T0 -> S0) : Set.
Check (nat -> nat).
Fail Check (forall A : Set, A -> A) : Set.
Check (Prop -> Prop) : Type.
Check (Set -> Set) : Type.
Check (forall A : Set, A -> A) : Type.
Check (nat -> Prop) : Type.
Check ((Prop -> Prop) -> Prop) : Type.
Check (forall P : nat -> Prop, Prop) : Type.
End product_formation.
Variable x : Prop.
Variables A B : Prop.
Variable t2 : Prop.
Check A -> B : Prop.
Check (fun y => y -> y) : Prop -> Prop.
Definition t1_oops := fun y => y -> y.
Check t1_oops.
Definition t1 := fun y : Prop => y -> y.
Check t1.
Check (t1 t2) : Prop.
Check (Prop -> Prop) -> B.
Fail Check (fun y : Prop => y -> y) -> B.
End minimal_Gallina_introduction.
From Ssreflect Require Import ssreflect.
Module propositions_as_types_example.
Lemma hilbertS (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
Show Proof.
move=> H1.
Show Proof. move=> H2.
move=> H3.
Show Proof.
cut B. Show Proof.
cut A.
Show Proof.
assumption.
assumption.
Show Proof.
cut A.
assumption.
assumption.
Show Proof.
Qed.
Definition hilbertS_proof :=
fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
(fun H : B => (fun H0 : A => H1 H0) H3 H) ((fun H : A => H2 H) H3).
Lemma hilbertS_direct_proof (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
exact (hilbertS_proof A B C).
Qed.
Lemma hilbertS_in_practice (A B C : Prop) :
(A -> B -> C) -> (A -> B) -> A -> C.
move=> H1.
move=> H2.
move=> H3.
apply H1.
exact H3.
apply H2.
exact H3.
Show Proof.
Qed.
Definition hilbertS_in_practice_proof :=
fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
H1 H3 (H2 H3).
Goal hilbertS_proof = hilbertS_in_practice_proof.
reflexivity.
Qed.
End propositions_as_types_example.
Module move_and_apply_tactics.
Lemma modus_ponens : forall P Q : Prop, (P -> Q) -> P -> Q.
Show Proof.
move=> P.
move: P.
move=> P Q PQ p.
move: PQ.
apply.
done.
Qed.
Goal forall P Q : Prop, (forall R : Prop, R -> Q) -> P -> Q.
Proof.
move=> P Q rq p.
Fail apply rq.
apply: rq p.
Qed.
Variable A : Prop.
Variable op : A -> A -> A.
Local Notation "a + b" := (op a b). Hypothesis opA : forall a b c, a + (b + c) = a + b + c.
Check opA.
Variable lt : A -> A -> Prop.
Local Notation "a < b" := (lt a b).
Hypothesis lt_addr : forall m n p, m < n -> m < n + p.
Goal forall a b c d,
a < b ->
a < b + c + d.
move=> a b c d.
Fail apply lt_addr.
rewrite -opA.
apply lt_addr.
Qed.
Goal False.
evar (x : nat).
have : (2 + x = 4 + 5)%nat.
rewrite /x.
apply refl_equal.
rewrite /= in x *.
Abort.
End move_and_apply_tactics.
Lemma exo0 : forall P : Prop, P -> P.
Proof.
Admitted.
Lemma exo1 : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
Admitted.
Lemma exo2 : forall P : Prop, (P -> P) -> P -> P.
Proof.
Admitted.
Lemma exo3 P Q R : (P -> Q) -> (Q -> R) -> P -> R.
Proof.
Admitted.
Section logical_connectives.
Print True.
Check True.
Check I.
Goal True.
apply: I.
Qed.
Print False.
Goal True -> False.
case.
Show Proof.
Abort.
Check False_ind.
Goal False -> 1 = 0.
move=> p.
exact: (False_ind (1 = 0) p).
Qed.
Goal False -> 1 = 0.
case.
Qed.
Print and.
Check conj I I.
Print and_ind.
Print and_rect.
Goal forall P Q, P /\ Q -> Q /\ P.
move=> P Q.
case.
Show Proof.
move=> p q.
split.
exact q.
exact p.
Qed.
Print or.
Check or_ind.
Check (or_intror False I).
About or_intror.
Check (@or_intror False True I).
Check (@or_intror False _ I).
Check (@or_intror _ _ I).
Check (@or_intror _ _ I) : False \/ True.
Goal forall A B, A \/ B -> B \/ A.
move=> A B.
case => [a | b].
right.
exact.
left.
exact b.
Qed.
End logical_connectives.
Lemma exo4 : False \/ True.
Proof.
Abort.
Lemma exo5 : forall A B C : Prop, A /\ B <-> B /\ A.
Proof.
move=> A B C.
Locate "<->".
Print iff.
Abort.
Lemma exo6 (A B C : Prop) : A /\ B /\ C ->
(A /\ B) /\ C.
Proof.
Abort.
Lemma exo7 (A B : Prop) : (A -> B) -> (~B -> ~A).
Proof.
Abort.
Section Set_Prop.
Check nat.
Goal 0 = 1 -> False.
move=> abs.
discriminate.
Qed.
Goal (exists n : nat, True) -> nat.
Fail case.
Abort.
About ex.
Goal forall A B : Prop, A \/ B -> nat.
move=> A B.
Fail case.
Abort.
Goal 0 = 1 -> nat.
move=> abs.
discriminate.
Show Proof.
Qed.
Goal forall n m : nat, n = m /\ n <> m -> nat.
move=> n m.
case => nm nm'.
exact O.
Qed.
Print sum.
Print sumbool.
Print sumor.
About sig.
Goal {n : nat | True} -> nat.
case.
move=> m _.
exact m.
Qed.
End Set_Prop.
Section product_formation.
Check Prop.
Check Set.
Set Printing Universes.
Check Type.
Unset Printing Universes.
Variables P0 P1 : Prop.
Check P0 -> P1 : Set.
Check P0 : Set.
Check P0 : Type.
Variable S0 : Set.
Check S0 : Type.
Check P1 -> P1 : Prop.
Check (S0 -> P0) : Prop.
Variable T0 : Type.
Check (T0 -> P0) : Prop.
Check (True -> True).
Check (forall x : nat, 0 <= x).
Check (forall x : nat, x = x) : Set.
Check (forall A : Prop, A -> A).
Check nat -> Prop.
Check (forall P : nat -> Prop, P O -> exists n : nat , P n) : Prop.
Check (P0 -> S0) : Set.
Fail Check (P0 -> S0) : Prop.
Variable S1 : Set.
Check (S1 -> S0) : Set.
Fail Check (T0 -> S0) : Set.
Check (nat -> nat).
Fail Check (forall A : Set, A -> A) : Set.
Check (Prop -> Prop) : Type.
Check (Set -> Set) : Type.
Check (forall A : Set, A -> A) : Type.
Check (nat -> Prop) : Type.
Check ((Prop -> Prop) -> Prop) : Type.
Check (forall P : nat -> Prop, Prop) : Type.
End product_formation.