forked from oysteikt/sf1-template
Complete ProofObjects.v
This commit is contained in:
+123
-38
@@ -172,10 +172,15 @@ Print ev_4'''.
|
||||
|
||||
Theorem ev_8 : ev 8.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
apply ev_SS.
|
||||
apply ev_SS.
|
||||
apply ev_SS.
|
||||
apply ev_SS.
|
||||
apply ev_0.
|
||||
Qed.
|
||||
|
||||
Definition ev_8' : ev 8
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition ev_8' : ev 8 :=
|
||||
ev_SS 6 (ev_SS 4 (ev_SS 2 (ev_SS 0 ev_0))).
|
||||
(** [] *)
|
||||
|
||||
(* ################################################################# *)
|
||||
@@ -396,8 +401,11 @@ Definition and_comm' P Q : P /\ Q <-> Q /\ P :=
|
||||
|
||||
Construct a proof object for the following proposition. *)
|
||||
|
||||
Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R :=
|
||||
fun P Q R HPQ HQR =>
|
||||
match (HPQ, HQR) with
|
||||
| (conj HP _, conj _ HR) => conj HP HR
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(* ================================================================= *)
|
||||
@@ -454,8 +462,14 @@ End Or.
|
||||
|
||||
Construct a proof object for the following proposition. *)
|
||||
|
||||
Definition or_commut' : forall P Q, P \/ Q -> Q \/ P
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Print or_comm.
|
||||
|
||||
Definition or_commut' : forall P Q, P \/ Q -> Q \/ P :=
|
||||
fun P Q HPQ =>
|
||||
match HPQ with
|
||||
| or_introl HP => or_intror HP
|
||||
| or_intror HQ => or_introl HQ
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(* ================================================================= *)
|
||||
@@ -500,8 +514,8 @@ Definition some_nat_is_even : exists n, ev n :=
|
||||
|
||||
Construct a proof object for the following proposition. *)
|
||||
|
||||
Definition ex_ev_Sn : ex (fun n => ev (S n))
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition ex_ev_Sn : ex (fun n => ev (S n)) :=
|
||||
ex_intro (fun n => ev (S n)) 1 (ev_SS 0 ev_0).
|
||||
(** [] *)
|
||||
|
||||
(** To destruct existentials in a proof term we simply use match: *)
|
||||
@@ -520,8 +534,11 @@ Definition dist_exists_or_term (X:Type) (P Q : X -> Prop) :
|
||||
Construct a proof object for the following proposition: *)
|
||||
Definition ex_match : forall (A : Type) (P Q : A -> Prop),
|
||||
(forall x, P x -> Q x) ->
|
||||
(exists x, P x) -> (exists x, Q x)
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
(exists x, P x) -> (exists x, Q x) :=
|
||||
fun P Q H HPQ HEP =>
|
||||
match HEP with
|
||||
| ex_intro _ x Hx => ex_intro _ x (HPQ x Hx)
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(* ================================================================= *)
|
||||
@@ -539,8 +556,8 @@ Inductive True : Prop :=
|
||||
|
||||
Construct a proof object for the following proposition. *)
|
||||
|
||||
Definition p_implies_true : forall P, P -> True
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition p_implies_true : forall P, P -> True :=
|
||||
fun P HP => I.
|
||||
(** [] *)
|
||||
|
||||
(** [False] is equally simple -- indeed, so simple it may look
|
||||
@@ -575,8 +592,8 @@ Definition false_implies_zero_eq_one : False -> 0 = 1 :=
|
||||
|
||||
Construct a proof object for the following proposition. *)
|
||||
|
||||
Definition ex_falso_quodlibet' : forall P, False -> P
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition ex_falso_quodlibet' : forall P, False -> P :=
|
||||
fun P HP => match HP with end.
|
||||
(** [] *)
|
||||
|
||||
End Props.
|
||||
@@ -674,8 +691,14 @@ Qed.
|
||||
matching on the equality hypotheses. *)
|
||||
|
||||
Definition eq_cons : forall (X : Type) (h1 h2 : X) (t1 t2 : list X),
|
||||
h1 == h2 -> t1 == t2 -> h1 :: t1 == h2 :: t2
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
h1 == h2 -> t1 == t2 -> h1 :: t1 == h2 :: t2 :=
|
||||
fun X h1 h2 t1 t2 Hheq Hteq =>
|
||||
match Hheq with
|
||||
| eq_refl h =>
|
||||
match Hteq with
|
||||
| eq_refl t => eq_refl (cons h t)
|
||||
end
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 2 stars, standard (equality__leibniz_equality)
|
||||
@@ -688,7 +711,11 @@ Definition eq_cons : forall (X : Type) (h1 h2 : X) (t1 t2 : list X),
|
||||
Lemma equality__leibniz_equality : forall (X : Type) (x y: X),
|
||||
x == y -> forall (P : X -> Prop), P x -> P y.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
intros X x y Heq P.
|
||||
destruct Heq as [x].
|
||||
intros Px.
|
||||
exact Px.
|
||||
Qed.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 2 stars, standard (equality__leibniz_equality_term)
|
||||
@@ -698,8 +725,11 @@ Proof.
|
||||
proof term constructed by tactics in the previous exercise is
|
||||
needessly complicated. Hint: pattern-match as soon as possible. *)
|
||||
Definition equality__leibniz_equality_term : forall (X : Type) (x y: X),
|
||||
x == y -> forall P : (X -> Prop), P x -> P y
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
x == y -> forall P : (X -> Prop), P x -> P y :=
|
||||
fun _ _ _ Heq _ =>
|
||||
match Heq with
|
||||
| eq_refl _ => fun Px => Px
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 3 stars, standard, optional (leibniz_equality__equality)
|
||||
@@ -712,7 +742,12 @@ Definition equality__leibniz_equality_term : forall (X : Type) (x y: X),
|
||||
Lemma leibniz_equality__equality : forall (X : Type) (x y: X),
|
||||
(forall P:X->Prop, P x -> P y) -> x == y.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
intros X x y Hleib.
|
||||
specialize (Hleib (fun x' => x == x')).
|
||||
simpl in Hleib.
|
||||
apply Hleib.
|
||||
apply (eq_refl x).
|
||||
Qed.
|
||||
(** [] *)
|
||||
|
||||
End EqualityPlayground.
|
||||
@@ -847,38 +882,66 @@ Fail Definition falso : False := infinite_loop 0.
|
||||
|
||||
(** **** Exercise: 2 stars, standard (and_assoc) *)
|
||||
Definition and_assoc : forall P Q R : Prop,
|
||||
P /\ (Q /\ R) -> (P /\ Q) /\ R
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
P /\ (Q /\ R) -> (P /\ Q) /\ R :=
|
||||
fun P Q R H =>
|
||||
match H with
|
||||
| conj HP (conj HQ HR) => conj (conj HP HQ) HR
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 3 stars, standard (or_distributes_over_and) *)
|
||||
Definition or_distributes_over_and : forall P Q R : Prop,
|
||||
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R)
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) :=
|
||||
fun P Q R =>
|
||||
let
|
||||
PQPR := fun (H : P \/ (Q /\ R)) =>
|
||||
match H with
|
||||
| or_introl HP => conj (or_introl HP) (or_introl HP)
|
||||
| or_intror (conj HQ HR) => conj (or_intror HQ) (or_intror HR)
|
||||
end
|
||||
in
|
||||
let
|
||||
PQR := fun (H : (P \/ Q) /\ (P \/ R)) =>
|
||||
match H with
|
||||
| conj (or_introl HP) _ => or_introl HP
|
||||
| conj _ (or_introl HP) => or_introl HP
|
||||
| conj (or_intror HQ) (or_intror HR) => or_intror (conj HQ HR)
|
||||
end
|
||||
in
|
||||
conj PQPR PQR.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 3 stars, standard (negations) *)
|
||||
Definition double_neg : forall P : Prop,
|
||||
P -> ~~P
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
P -> ~~P :=
|
||||
fun P HP HNP => HNP HP.
|
||||
|
||||
Definition contradiction_implies_anything : forall P Q : Prop,
|
||||
(P /\ ~P) -> Q
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
(P /\ ~P) -> Q :=
|
||||
fun P Q H =>
|
||||
match H with
|
||||
| conj HP HNP => match HNP HP with end
|
||||
end.
|
||||
|
||||
Definition de_morgan_not_or : forall P Q : Prop,
|
||||
~ (P \/ Q) -> ~P /\ ~Q
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
~ (P \/ Q) -> ~P /\ ~Q :=
|
||||
fun P Q H =>
|
||||
conj
|
||||
(fun HP => H (or_introl HP))
|
||||
(fun HQ => H (or_intror HQ)).
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 2 stars, standard (currying) *)
|
||||
Definition curry : forall P Q R : Prop,
|
||||
((P /\ Q) -> R) -> (P -> (Q -> R))
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
((P /\ Q) -> R) -> (P -> (Q -> R)) :=
|
||||
fun P Q R H HP HQ => H (conj HP HQ).
|
||||
|
||||
Definition uncurry : forall P Q R : Prop,
|
||||
(P -> (Q -> R)) -> ((P /\ Q) -> R)
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
(P -> (Q -> R)) -> ((P /\ Q) -> R) :=
|
||||
fun P Q R H H' =>
|
||||
match H' with
|
||||
| conj HP HQ => H HP HQ
|
||||
end.
|
||||
(** [] *)
|
||||
|
||||
(* ################################################################# *)
|
||||
@@ -906,7 +969,16 @@ Theorem pe_implies_or_eq :
|
||||
propositional_extensionality ->
|
||||
forall (P Q : Prop), (P \/ Q) = (Q \/ P).
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
intros PE P Q.
|
||||
apply PE.
|
||||
split.
|
||||
- intros [HP | HQ].
|
||||
+ right. apply HP.
|
||||
+ left. apply HQ.
|
||||
- intros [HQ | HP].
|
||||
+ right. apply HQ.
|
||||
+ left. apply HP.
|
||||
Qed.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 1 star, advanced (pe_implies_true_eq)
|
||||
@@ -917,7 +989,13 @@ Proof.
|
||||
Lemma pe_implies_true_eq :
|
||||
propositional_extensionality ->
|
||||
forall (P : Prop), P -> True = P.
|
||||
Proof. (* FILL IN HERE *) Admitted.
|
||||
Proof.
|
||||
intros PE P HP.
|
||||
apply PE.
|
||||
split.
|
||||
- intros _. apply HP.
|
||||
- intros _. apply I.
|
||||
Qed.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 3 stars, advanced (pe_implies_pi)
|
||||
@@ -940,7 +1018,14 @@ Definition proof_irrelevance : Prop :=
|
||||
|
||||
Theorem pe_implies_pi :
|
||||
propositional_extensionality -> proof_irrelevance.
|
||||
Proof. (* FILL IN HERE *) Admitted.
|
||||
Proof.
|
||||
unfold propositional_extensionality, proof_irrelevance.
|
||||
intros PE P pf1 pf2.
|
||||
pose proof (pe_implies_true_eq PE P pf1) as H.
|
||||
subst P.
|
||||
destruct pf1, pf2.
|
||||
reflexivity.
|
||||
Qed.
|
||||
(** [] *)
|
||||
|
||||
(* 2026-01-07 13:18 *)
|
||||
|
||||
Reference in New Issue
Block a user