PRFA.tp5c
MPRI 2-7-2 / 2023 / Exercise session 7 / Solutions
Sorts
Inductive prop_bool : Prop := ptrue | pfalse.
Definition to_prop_bool (b : bool) : prop_bool :=
if b then ptrue else pfalse.
ANSWER
We can't go the other way because we cannot eliminate from Prop to Type.
This would contradict axioms like proof irrelevance. Even though proof
irrelevance is not assumed, Coq is built so that assuming remains
consistent.
Lemma from_prop_bool_neg_PI :
∀ (f : prop_bool → bool),
(∀ b, b = f (to_prop_bool b)) →
¬ (∀ (P : Prop) (u v : P), u = v).
Proof.
intros f hf PI.
specialize (PI prop_bool ptrue pfalse).
specialize (hf true) as e1.
specialize (hf false) as e2.
simpl in ×.
rewrite PI in e1. rewrite <- e2 in e1. discriminate.
Qed.
EXERCISE
Prove that for all p : prop_bool, there exists some b : bool such that
its mapping to prop_bool is equal to p.
Lemma to_bool :
∀ (p : prop_bool),
∃ (b : bool), to_prop_bool b = p.
Proof.
intros [].
- ∃ true. reflexivity.
- unshelve eexists ; econstructor.
Qed.
EXERCISE
exists (x : A), P x and { x : A | P x } are two very similar types but the
former lives in Prop. Show how one implies the other.
Lemma to_exists :
∀ A (P : A → Prop),
{ x : A | P x } →
∃ x, P x.
Proof.
intros A P [x h].
∃ x. assumption.
Qed.
EXERCISE
Similarly, P \/ Q and A + B are similar types. The first you know as
disjunction of propositions, the other one is relevant data that either
contains either a value of type A, or a value of type B.
Prove that P + Q -> P \/ Q, ideally with a proof term.
Locate "+".
Print sum.
Definition to_disj {P Q : Prop} (x : P + Q) : P ∨ Q :=
match x with
| inl p ⇒ or_introl p
| inr q ⇒ or_intror q
end.
EXERCISE
We can't show that (exists x, P x) -> { x : A | P x } in general, but we can
when A is bool and when P x is of the form f x = true. Show it.
Lemma to_sig_bool :
∀ (f : bool → bool),
(∃ b, f b = true) →
{ b | f b = true }.
Proof.
intros f h.
destruct (f true) eqn: etrue.
- ∃ true. assumption.
- ∃ false.
destruct h as [b e].
destruct b.
+ rewrite e in etrue. discriminate.
+ assumption.
Qed.
Singleton elimination
EXERCISE
Write a term that goes from False to any A : Type.
EXERCISE
Write a term that given P : A -> Type and e : u = v goes from P u to P v.
You will see better why it is useful next week.
Definition transport {A} (P : A → Type) {u v} (e : u = v) (t : P u) : P v :=
match e with
| eq_refl ⇒ t
end.
EXERCISE
We have seen above that disjunction was not a singleton. What about
conjunction?
EXERCISE
Propose a version of le that is a singleton.
You can use the goal below with le (<=) and with your le'.
It should only work with le'.
Is it satisfying?
Goal ∀ n m, n ≤ m → nat.
Proof.
intros n m h.
Fail destruct h.
Abort.
Inductive le' (n m : nat) : Prop :=
| le_intro : (n = m ∨ le' n (pred m)) → le' n m.
Goal ∀ n m, le' n m → nat.
Proof.
intros n m h.
destruct h.
We can't actually do much, it's a bit like Box in the end.
Abort.
Alternatively we can define le with a fixpoint to actually extract info.
Fixpoint le_alt (n m : nat) : Prop :=
match n, m with
| 0, _ ⇒ True
| S n, 0 ⇒ False
| S n, S m ⇒ le_alt n m
end.
But then, we're not really destructing the proof, but rather the integers.
In particular, we can't perform induction on the proof itself.
Fixpoint le_dec n m : { le_alt n m } + { ¬ le_alt n m } :=
match n, m with
| 0, _ ⇒ left I
| S n, 0 ⇒ right (fun x ⇒ x)
| S n, S m ⇒ le_dec n m
end.
(*** Induction principles ***)
EXERCISE
Define an inductive type bintree for binary trees.
As for every inductive type, Coq generates induction principles corresponding
to the various sorts:
- bintree_ind for Prop
- bintree_rect for Type
- bintree_rec for Set (but you can ignore it and use bintree_rect)
Inductive bintree A :=
| bt_leaf (a : A)
| bt_node (a : A) (l r : bintree A).
Arguments bt_leaf {A}.
Arguments bt_node {A}.
Check bintree_rect.
EXERCISE
Define a map function for it, and show mapping with the identity results in
the identity on binary trees.
Fixpoint bt_map {A B} (f : A → B) (t : bintree A) : bintree B :=
match t with
| bt_leaf a ⇒ bt_leaf (f a)
| bt_node a l r ⇒ bt_node (f a) (bt_map f l) (bt_map f r)
end.
Lemma bt_map_id :
∀ A (t : bintree A),
bt_map (fun x ⇒ x) t = t.
Proof.
intros A t.
induction t as [a | a l ihl r ihr].
- reflexivity.
- cbn. rewrite ihl, ihr. reflexivity.
Qed.
EXERCISE
Define an inductive type tree of trees taking a list of children.
- Show that all binary trees can be seen as trees.
- Define a map function for tree.
- Show that turning a binary tree into a tree then mapping is the same as mapping first then turning into a tree.
Inductive tree A :=
| node (a : A) (children : list (tree A)).
Arguments node {A}.
Fixpoint bt_to_tree {A} (t : bintree A) : tree A :=
match t with
| bt_leaf a ⇒ node a []
| bt_node a l r ⇒ node a [ bt_to_tree l ; bt_to_tree r ]
end.
Fixpoint tree_map {A B} (f : A → B) (t : tree A) : tree B :=
match t with
| node a l ⇒ node (f a) (map (tree_map f) l)
end.
Lemma to_tree_map :
∀ A B (f : A → B) t,
tree_map f (bt_to_tree t) = bt_to_tree (bt_map f t).
Proof.
intros A B f t.
induction t as [a | a l ihl r ihr].
- reflexivity.
- cbn. rewrite ihl, ihr. reflexivity.
Qed.
EXERCISE
Now if you want to show that mapping with the identity on tree results in
the identity function, you will be in trouble because
tree_ind (use Check or About to see its type)
does not carry any induction hypothesis.
Taking inspiration from tree_ind, implement some good_tree_ind that has an
induction hypothesis for the list of children.
Hint: You may use the Forall P l which says that P x holds for every x in l.
To do the proof, you can use the tactic fix like
fix ind 1
to perform recursion on the first argument in the goal and call
ind the recursive call.
You will need to do to nested fixpoints, one for the tree and one for the list
of children.
This is hard to get right, so you can also admit it and move on.
Check tree_ind.
Lemma good_tree_ind :
∀ A (P : tree A → Prop),
(∀ a l, Forall P l → P (node a l)) →
∀ t, P t.
Proof.
intros A P h.
fix ind 1.
intros [ a l ].
apply h.
revert l. fix aux 1. intro l.
destruct l as [| x l].
- constructor.
- constructor.
+ apply ind.
+ apply aux.
Qed.
EXERCISE
Use induction using good_tree_ind to prove that mapping with the identity
function on tree results in the identity function.
Lemma tree_map_id :
∀ A (t : tree A),
tree_map (fun x ⇒ x) t = t.
Proof.
intros A t.
induction t as [a l ihl] using good_tree_ind.
cbn. f_equal. induction ihl.
- reflexivity.
- cbn. f_equal. all: assumption.
Qed.
EXERCISE Strong induction on natural numbers
We have seen it already, but show it again and use it to prove the following
lemma that corresponds to induction on natural numbers with access to the
two previous cases.
Lemma strong_nat_ind :
∀ (P : nat → Prop),
(∀ n, (∀ m, m < n → P m) → P n) →
∀ n, P n.
Proof.
intros P h n.
apply h.
induction n as [| n ih].
- intros m hm. inversion hm.
- intros m hm. inversion hm.
+ apply h. assumption.
+ apply ih. lia.
Qed.
Lemma nat_ind_2 :
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n, P n → P (S n) → P (S (S n))) →
∀ n, P n.
Proof.
intros P h0 h1 hSS n.
induction n as [n ih] using strong_nat_ind.
destruct n as [| [| n]]. 1,2: assumption.
apply hSS.
all: apply ih. all: lia.
Qed.
EXERCISE
Use the induction tactic with nat_ind_2 to prove that the fibonacci sequence
is always above its index (n <= fib n).
Fixpoint fib n :=
match n with
| 0 ⇒ 1
| 1 ⇒ 1
| S (S n as m) ⇒ fib n + fib m
end.
Lemma fib_superlinear :
∀ n, n ≤ fib n.
Proof.
intros n.
induction n as [| | n hn hSn] using nat_ind_2.
- simpl. auto.
- simpl. auto.
- change (fib (S (S n))) with (fib n + fib (S n)).
destruct n.
+ simpl. auto.
+ lia.
Qed.
Well-founded induction
We are going to show that for any decidable predicate P with ∃ n, P n we
can compute a natural number n for which P holds, i.e. deduce { n | P n
}.
Section ConstructiveIndefiniteGroundDescription_Acc.
Variable P : nat → Prop.
Hypothesis P_decidable : ∀ n : nat, {P n} + {¬ P n}.
Let R (x y : nat) : Prop := x = S y ∧ ¬ P y.
Local Notation acc x := (Acc R x).
Lemma P_implies_acc : ∀ x : nat, P x → acc x.
Proof.
intros x H. constructor.
intros y [_ not_Px]. absurd (P x); assumption.
Qed.
Lemma P_eventually_implies_acc : ∀ (x : nat) (n : nat), P (n + x) → acc x.
Proof.
intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
- apply P_implies_acc.
- intros x H. constructor. intros y [fxy _].
apply IH. rewrite fxy.
replace (n + S x) with (S (n + x)) by lia.
assumption.
Qed.
Corollary P_eventually_implies_acc_ex : (∃ n : nat, P n) → acc 0.
Proof.
intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
replace (x + 0) with x by lia.
assumption.
Qed.
Theorem acc_implies_P_eventually : acc 0 → {n : nat | P n}.
Proof.
intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption].
clear Acc_0; intros x IH.
destruct (P_decidable x) as [Px | not_Px].
- ∃ x; simpl; assumption.
- set (y := S x).
assert (Ryx : R y x).
+ unfold R; split; auto.
+ destruct (IH y Ryx) as [n Hn].
∃ n; assumption.
Qed.
Theorem constructive_indefinite_ground_description_nat_Acc :
(∃ n : nat, P n) → {n : nat | P n}.
Proof.
intros H; apply acc_implies_P_eventually.
apply P_eventually_implies_acc_ex; assumption.
Qed.
End ConstructiveIndefiniteGroundDescription_Acc.
We have seen well-founded induction, but sometimes we also want to define
functions like that. The standard library comes with a helpful function for
doing that called Fix_F. It performs induction on accessibilty like we have
been doing.
EXERCISE
Implement a merge function on lists such that if l and r are individually
sorted, then merge l r should be sorted too.
This function is the main ingredient for the merge sort algorithm.
We give you the version one would write in OCaml and you have to adapt it into
a function accepted by Coq.
We're using lists of natural numbers to make it simpler but it could be
generalised of course.
Hint: You may have to pack arguments together to make it work.
Next, prove a specification for merge that ensures it preserves sortedness
and that the result is a permutation of the original lists. You can use a
weak version of permutation that doesn't account for multiplicity.
We give you some lemmas about sorted and wpermut that you may or may not use.
This is so you don't waste too much time on those. We expect you to begin
by admitting them, but you should be able to prove them.
Hint: If you want to do induction on Acc, you better prove a better induction
principle for it because the one generated isn't enough.
Fail Fixpoint merge (l r : list nat) : list nat :=
match l, r with
| [], r ⇒ r
| l, [] ⇒ l
| x :: l, y :: r ⇒
if x <? y
then x :: merge l (y :: r)
else y :: merge (x :: l) r
end.
Inductive sorted : list nat → Prop :=
| sorted_nil : sorted []
| sorted_cons : ∀ x l, sorted l → Forall (le x) l → sorted (x :: l).
Definition wpermut (l r : list nat) : Prop :=
∀ x, In x l ↔ In x r.
Lemma Acc_rect_dep :
∀ [A] [R : A → A → Prop] (P : ∀ a, Acc R a → Type),
(∀ x (h : ∀ y, R y x → Acc R y),
(∀ y hy, P y (h y hy)) →
P x (Acc_intro x h)
) →
∀ x a, P x a.
Proof.
intros A R P h.
fix ind 2. intros x a.
destruct a as [ha].
apply h. intros. apply ind.
Defined.
#[export] Instance wpermut_refl : Reflexive wpermut.
Proof.
intros l x. reflexivity.
Qed.
#[export] Instance wpermut_sym : Symmetric wpermut.
Proof.
intros l r h x. symmetry. apply h.
Qed.
#[export] Instance wpermut_trans : Transitive wpermut.
Proof.
intros a b c h1 h2 x. transitivity (In x b).
- apply h1.
- apply h2.
Qed.
Add Parametric Relation : (list nat) wpermut as wpermut_rel.
Lemma Forall_wpermut :
∀ P l r,
wpermut l r →
Forall P r →
Forall P l.
Proof.
intros P l r hp h.
rewrite Forall_forall. rewrite Forall_forall in h.
intros x hx.
unfold wpermut in hp. rewrite hp in hx. auto.
Qed.
Lemma wpermut_cons :
∀ x l r,
wpermut l r →
wpermut (x :: l) (x :: r).
Proof.
intros x l r h.
unfold wpermut in ×. simpl.
intros y. rewrite h. reflexivity.
Qed.
Lemma wpermut_app :
∀ l r,
wpermut (l ++ r) (r ++ l).
Proof.
intros l r x.
rewrite !in_app_iff. rewrite or_comm. reflexivity.
Qed.
Lemma sorted_cons_inv :
∀ x l,
sorted (x :: l) →
sorted l ∧ Forall (le x) l.
Proof.
intros x l h.
inversion h. auto.
Qed.
Section Merge.
Let T := (list nat × list nat)%type.
Let m (x : T) := length (fst x) + length (snd x).
Let R (x y : T) := S (m x) = m y.
Lemma merge_acc :
∀ x, Acc R x.
Proof.
intro x.
remember (m x) as n eqn:e.
induction n as [| n ih] in x, e |- ×.
- constructor. intros y hr.
unfold R in hr. rewrite <- e in hr. inversion hr.
- constructor. intros y hr.
unfold R in hr. apply ih. lia.
Qed.
Lemma R_step2 :
∀ x y l r,
R (x :: l, r) (x :: l, y :: r).
Proof.
intros x y l r.
unfold R. cbn. lia.
Qed.
Definition merge (x : T) : list nat :=
Fix_F _ (fun x rec ⇒
match x with
| ([], l) | (l, []) ⇒ fun rec ⇒ l
| (x :: l, y :: r) ⇒ fun (rec : ∀ z, R z (x :: l, y :: r) → list nat) ⇒
if x <? y
then x :: rec (l, y :: r) eq_refl
else y :: rec (x :: l, r) (R_step2 _ _ _ _)
end rec
) (merge_acc x).
Lemma merge_spec :
∀ l r,
sorted l →
sorted r →
sorted (merge (l, r)) ∧ wpermut (merge (l, r)) (l ++ r).
Proof.
intros l r hl hr.
unfold merge.
set (a := merge_acc _). clearbody a.
remember (l, r) as t eqn:e.
lazymatch goal with
| |- context [ Fix_F _ ?G _ ] ⇒ set (F := G)
end.
induction a as [t h ih] using Acc_rect_dep in l, r, e, hl, hr |- ×.
simpl. subst.
destruct l as [| x l], r as [| y r].
all: simpl.
1-3: intuition eauto. 3: rewrite app_nil_r.
1-3: reflexivity.
destruct (x <? y) eqn: e.
- apply sorted_cons_inv in hl as [hl hxl].
specialize ih with (1 := hl) (2 := hr) (3 := eq_refl).
specialize (ih eq_refl).
destruct ih as [ihs ihp].
split.
+ constructor. 1: assumption.
eapply Forall_wpermut. 1: eassumption.
apply sorted_cons_inv in hr as [hr hyr].
apply Forall_app. intuition auto.
apply Nat.leb_le in e.
constructor. 1: lia.
eapply Forall_impl. 2: eassumption.
lia.
+ apply wpermut_cons. assumption.
- specialize ih with (hy := R_step2 x y l r).
specialize ih with (3 := eq_refl).
apply sorted_cons_inv in hr as [hr hyr].
specialize (ih hl hr).
destruct ih as [ihs ihp].
split.
+ constructor. 1: assumption.
eapply Forall_wpermut. 1: eassumption.
apply sorted_cons_inv in hl as [hl hxl].
apply Forall_app. intuition auto.
apply Nat.ltb_ge in e.
constructor. 1: lia.
eapply Forall_impl. 2: eassumption.
lia.
+ change (x :: l ++ y :: r) with ((x :: l) ++ (y :: r)).
rewrite wpermut_app. simpl.
apply wpermut_cons.
rewrite wpermut_app. assumption.
Qed.
End Merge.
ADVANCED EXERCISES
inhabited A is just a proposition from which you cannot extract the
witness.
If there is an element verifying the property, then the one epsilon gave
us also verifies it.
We also need some extensionality to tell us that the choice does not
depend on how the property was formulated.
EXERCISE
Prove the excluded middle.
Hint: You can use epsilon with some property like x = true \/ P and same
with false.
Lemma epsilon_LEM :
∀ (P : Prop), P ∨ ¬ P.
Proof.
intro P.
pose (i := inhabits true).
pose (B := fun x ⇒ x = false ∨ P).
pose (C := fun x ⇒ x = true ∨ P).
pose (b := epsilon bool i B).
pose (c := epsilon bool i C).
assert (hb : B b).
{ apply epsilon_spec. ∃ false. left. reflexivity. }
assert (hc : C c).
{ apply epsilon_spec. ∃ true. left. reflexivity. }
destruct hb as [eb | hP]. 2: auto.
destruct hc as [ec | hP]. 2: auto.
right. intro hP.
assert (e : b = c).
{ apply epsilon_ext. intro x. unfold B, C. split. all: auto. }
rewrite eb, ec in e. discriminate.
Qed.
End Hilbert.
From relation to function
Another version of the axiom of choice says that from a entire relation,
one can extract a function. It's a form of inversion of quantifiers.
Definition fun_choice :=
∀ A B (R : A → B → Prop),
(∀ x, ∃ y, R x y) →
∃ (f : A → B),
∀ x, R x (f x).
EXERCISE
Show that fun_choice implies LEM as well.
You may use proposition and function extensionality.
Remember that it is enough to get PredExt and PI.
The proof should share some ideas with the one above and could involve some
function from { p : bool -> Prop | p = B \/ p = C } -> bool
with carefully chosen B and C.
Definition FunExt :=
∀ A B (f g : A → B),
(∀ x, f x = g x) →
f = g.
Definition PropExt :=
∀ (P Q : Prop), P ↔ Q → P = Q.
Lemma fun_choice_LEM :
fun_choice →
FunExt →
PropExt →
∀ (P : Prop), P ∨ ¬ P.
Proof.
intros ac funext propext P.
pose (B x := x = false ∨ P).
pose (C x := x = true ∨ P).
pose proof (ac { p | p = B ∨ p = C } bool (fun p b ⇒ proj1_sig p b)) as eps.
destruct eps as [f hf].
{ intros [p [eB | eC]].
- subst. simpl. ∃ false. left. reflexivity.
- subst. simpl. ∃ true. left. reflexivity.
}
specialize (hf ltac:(∃ B ; auto)) as hfB. simpl in hfB.
specialize (hf ltac:(∃ C ; auto)) as hfC. simpl in hfC.
destruct hfB as [eB | hP]. 2: auto.
destruct hfC as [eC | hP]. 2: auto.
right. intro hP.
assert (e : B = C).
{ apply funext. intro. apply propext. unfold B, C. split. all: auto. }
clearbody B C. subst.
assert (pi : ∀ (P : Prop) (p q : P), p = q).
{ intros Q u v.
assert (Q = True).
{ apply propext. split ; auto. }
subst.
destruct u, v. reflexivity.
}
assert (true = false).
{ rewrite <- eC, <- eB.
unshelve setoid_rewrite (pi (C = C ∨ C = C)).
3: reflexivity. auto.
}
discriminate.
Qed.