PRFA.tp7c
MPRI 2-7-2 — Proof assistants - Lesson 4 - Solutions
Module Leibniz.
Definition leib_eq {A} (u v : A) :=
∀ P, P u → P v.
Notation "u == v" := (leib_eq u v) (at level 80).
Definition refl {A} (a : A) : a == a :=
fun P (h : P a) ⇒ h.
Definition sym {A} (u v : A) (e : u == v) : v == u :=
fun P ⇒ e (fun x ⇒ P x → P u) (refl u P).
Definition trans {A} (u v w : A) (e : u == v) (e' : v == w) : u == w :=
fun P ⇒ e' (fun x ⇒ P u → P x) (e P).
Definition f_equal {A B} (f : A → B) {u v} (e : u == v) : f u == f v :=
fun P ⇒ e (fun x ⇒ P (f x)).
Lemma n_plus_0 : ∀ n, n + 0 == n.
Proof.
intro n. induction n as [ | n ih ].
- apply refl.
- simpl. apply f_equal. assumption.
Qed.
Lemma nat_discr : ∀ n, S n == 0 → False.
Proof.
intros n e.
specialize (e (fun x ⇒ match x with 0 ⇒ False | _ ⇒ True end)).
simpl in e. apply e. constructor.
Qed.
(* Coq's definition of equality, written = *)
Print eq.
(* Similar to Leibniz equality above *)
About eq_rect.
EXERCISE
Show equivalence of Leibniz equality and eq using eq_rect not rewrite or
destruct. In other words we want to see a proof of u = v <-> u == v.
You can use refine if it helps.
SORRY: As many of you noticed, currently, u == v is in Type and not in
Prop so you cannot use <->. You can put it in Prop by writing
Definition leib_eq {A} (u v : A) :=
forall (P : A -> Prop), P u -> P v.
Or you can prove the two arrows as below.
Definition eq_to_leib {A} (u v : A) (e : u = v) : u == v :=
eq_rect _ (fun x ⇒ u == x) (refl u) _ e.
Definition leib_to_eq {A} (u v : A) (e : u == v) : u = v :=
e (fun x ⇒ u = x) eq_refl.
End Leibniz.
(* Now we're only going to use eq from the standard library. *)
(* Similar to eq_rect but for propositions *)
About eq_ind.
EXERCISE
Show symmetry, transitivty and congruence (f_equal) for eq, once using
eq_ind / eq_rect and once using pattern matching on equality.
Definition eq_sym {A} {u v : A} (e : u = v) : v = u :=
eq_ind _ (fun x ⇒ x = u) eq_refl _ e.
Definition eq_trans {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
eq_ind _ (fun x ⇒ u = x) e _ e'.
Definition eq_sym' {A} {u v : A} (e : u = v) : v = u :=
match e with
| eq_refl ⇒ eq_refl
end.
Definition eq_trans' {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
match e with
| eq_refl ⇒ fun e' ⇒ e'
end e'.
Lemma f_equal' :
∀ A B (f : A → B) u v, u = v → f u = f v.
Proof.
intros A B f u v e.
destruct e. reflexivity.
Qed.
Definition f_equal_term A B (f : A → B) u v (e : u = v) : f u = f v :=
eq_ind _ (fun x ⇒ f u = f x) eq_refl _ e.
Definition f_equal_term' A B (f : A → B) u v (e : u = v) : f u = f v :=
match e with
| eq_refl ⇒ eq_refl
end.
EXERCISE
Identify the parameters and indices of eq. Then consider the definition of
equality eq_ts with rules for transitivity and symmetry below. What are the
parameters and indices? Why?
Show that eq and eq_ts are equivalent.
Inductive eq_ts {X} : X → X → Prop :=
| refl_eq x : eq_ts x x
| trans_eq x y z : eq_ts x y → eq_ts y z → eq_ts x z
| sym_eq x y : eq_ts x y → eq_ts y x.
The parameters in eq A u v are A and u, while v is an index.
Indeed, only the value of v is dictated by the constructor.
For eq_ts A u v, u is also an idex because of the symmetry rule.
Although it could be considered a parameter by writing
sym_eq x y : eq_ts y x -> eq_ts x y
instead.
Lemma eq_to_ts :
∀ A (u v : A),
u = v →
eq_ts u v.
Proof.
intros A u v e. subst. apply refl_eq.
Qed.
Lemma eq_from_ts :
∀ A (u v : A),
eq_ts u v →
u = v.
Proof.
intros A u v e.
induction e.
- reflexivity.
- transitivity y. all: assumption.
- symmetry. assumption.
Qed.
EXERCISE
Show a lemma similar to f_equal but for dependent functions, ie functions of
type forall (x : A), B x.
Hint: use eq_rect to state the lemma.
Lemma dep_f_equal :
∀ A B (f : ∀ (x : A), B x) u v (e : u = v),
eq_rect _ B (f u) _ e = f v.
Proof.
intros A B f u v e.
destruct e.
simpl. (* Notice how eq_rect computes! *)
reflexivity.
Qed.
EXERCISE
Define the inductive predicate for even natural numbers we already saw several
times (try to do it without having to look it up).
Then prove that even (S (S n)) implies even n. Try to do it using tactics
(for instance using the remember tactic) and by writing a proof term directly.
Do the same to prove that even 1 is false.
Finally, show that n cannot be even at the same time as S n.
(This time you can just do it using tactics.)
Inductive even : nat → Prop :=
| even0 : even 0
| evenS : ∀ n, even n → even (S (S n)).
Lemma evenSS_inv :
∀ n,
even (S (S n)) →
even n.
Proof.
intros n h.
destruct h. (* Coq forgot everything! *)
Restart.
intros n h.
remember (S (S n)) as m eqn: e.
destruct h.
- discriminate.
- inversion e. subst. assumption.
Qed.
Definition evenSS_inv_alt n (h : even (S (S n))) : even n :=
match h in even m return m = S (S n) → even n
with
| even0 ⇒
fun (e : 0 = S (S n)) ⇒
eq_ind 0 (fun x ⇒ match x with 0 ⇒ True | _ ⇒ even n end) I _ e
| evenS m h' ⇒
fun (e : S (S m) = S (S n)) ⇒
eq_ind _ even h' _ (f_equal (fun x ⇒ pred (pred x)) e)
end eq_refl.
Lemma not_even1 : ¬ even 1.
Proof.
intro h.
remember 1 as n eqn: e.
destruct h.
- discriminate.
- discriminate.
Qed.
Definition not_even1_term (h : even 1) : False :=
match h in even n return n = 1 → False
with
| even0 ⇒
fun (e : 0 = 1) ⇒
eq_ind 0 (fun x ⇒ match x with 0 ⇒ True | _ ⇒ False end) I _ e
| evenS m h' ⇒
fun (e : S (S m) = 1) ⇒
eq_ind (S (S m)) (fun x ⇒ match x with S (S n) ⇒ True | _ ⇒ False end) I _ e
end eq_refl.
Lemma even_and_S_False :
∀ n,
even n →
even (S n) →
False.
Proof.
intros n hn hSn.
induction hn in hSn |- ×.
- apply not_even1. assumption.
- apply IHhn. apply evenSS_inv. assumption.
Qed.
EXERCISE
Define the map function on lists. (We give you some lines so that you can
use the notations ☐ for nil and :: for cons.)
Show that map (fun x => x) l is the same as l.
Can you prove that map (fun x => x) is equal to the identity function?
From Coq Require Import List.
Import ListNotations.
Fixpoint map {A B} (f : A → B) (l : list A) : list B :=
match l with
| [] ⇒ []
| x :: l' ⇒ f x :: map f l'
end.
Lemma map_id :
∀ A (l : list A),
map (fun x ⇒ x) l = l.
Proof.
intros A l.
induction l.
- reflexivity.
- simpl. f_equal. assumption.
Qed.
Lemma map_id' :
∀ A,
map (fun (x : A) ⇒ x) = (fun l ⇒ l).
Proof.
intro A.
(* We're actually stuck here! *)
Abort.
(* Equality principles *)
EXERCISE
We give some equality principles below. You may assume some of them when
solving the exercises below. Try to assume only what you need.
Show that inhabited propositions are equal to True.
Similarly, show that uninhabited types are equal to False.
Show that two predicates are equal as soon as they are logically equivalent:
ie. as soon as forall x, P x <-> Q x.
Show that proof irrelevance follows from proposition extensionality.
Show that UIP follows from proof irrelevance.
Show that UIP and K are equivalent.
ERRATUM: The definition of K was wrong, sorry.
Definition FunExt :=
∀ A B (f g : A → B), (∀ x, f x = g x) → f = g.
Definition PropExt :=
∀ (P Q : Prop), (P ↔ Q) → P = Q.
Definition ProofIrrelevance :=
∀ (P : Prop) (p q : P), p = q.
Definition UIP :=
∀ A (u v : A) (p q : u = v), p = q.
Definition K :=
∀ A (u : A) (e : u = u), e = eq_refl.
Axiom funext : FunExt.
Lemma map_id' :
∀ A,
map (fun (x : A) ⇒ x) = (fun l ⇒ l).
Proof.
intro A.
apply funext. intro l.
apply map_id.
Qed.
Axiom propext : PropExt.
Lemma inhabited_is_True :
∀ (P : Prop), P → P = True.
Proof.
intros P h.
apply propext. split.
- intro. constructor.
- intro. assumption.
Qed.
Lemma neg_eq_False :
∀ (P : Prop), ¬ P → P = False.
Proof.
intros P h.
apply propext. split.
- assumption.
- intro bot. destruct bot.
Qed.
Lemma predext :
∀ A (P Q : A → Prop),
(∀ x, P x ↔ Q x) →
P = Q.
Proof.
intros A P Q h.
apply funext. intro x.
apply propext. apply h.
Qed.
Lemma proof_irrelevance :
(* using PropExt axiom *)
ProofIrrelevance.
Proof.
intros P H1 H2.
pose proof (inhabited_is_True P H1).
subst. destruct H1, H2.
reflexivity.
Qed.
Print Assumptions proof_irrelevance.
Definition PI_UIP : ProofIrrelevance → UIP.
Proof.
intros pi A u v p q.
apply pi.
Qed.
Definition UIP_K : UIP → K.
Proof.
intros uip A u e.
apply uip.
Qed.
Definition K_UIP : K → UIP.
Proof.
intros k A u v p q.
destruct q. apply k.
Qed.
EXERCISE
Define boolean equality for natural numebers, ie some
eq_nat : nat -> nat -> bool.
(You may have already done it, but try to do it again.)
Show that when eq_nat n m is true, then n = m.
Show that when it is false, then n <> m.
Deduce that equality of natural numbers is decidable.
This is typically achieved by defining
eq_dec : forall n m, { n = m } + { n <> m }.
You can first do it with tactics but try to do it with a proof term.
To know more about the {} + {} type, execute the following commands.
Locate can tell you what is the name of an object or notation.
Print for an inductive will tell you the name and type of its constructors.
Fixpoint eq_nat (n m : nat) : bool :=
match n, m with
| 0, 0 ⇒ true
| S n, S m ⇒ eq_nat n m
| _, _ ⇒ false
end.
Lemma eq_nat_eq :
∀ n m, eq_nat n m = true → n = m.
Proof.
intros n m.
induction n in m |- ×.
- destruct m. 2: discriminate.
reflexivity.
- destruct m. 1: discriminate.
intro e. f_equal. apply IHn. assumption.
Qed.
Lemma eq_eq_nat :
∀ n m, n = m → eq_nat n m = true.
Proof.
intros n m.
induction n in m |- ×.
- destruct m. 2: discriminate.
reflexivity.
- destruct m. 1: discriminate.
intro e. simpl. apply IHn.
inversion e. reflexivity.
Qed.
Lemma eq_dec :
∀ (n m : nat), { n = m } + { n ≠ m }.
Proof.
intros n m.
destruct (eq_nat n m).
- left. (* We don't know eq_nat n m = true here! *)
Restart.
intros n m.
destruct (eq_nat n m) eqn: e.
- left. apply eq_nat_eq. assumption.
- right. intro e'. apply eq_eq_nat in e'.
rewrite e' in e. discriminate.
Qed.
Locate "{ _ } + { _ }".
Print sumbool.
Lemma eq_nat_false :
∀ n m, eq_nat n m = false → n ≠ m.
Proof.
intros n m e. intro e'.
apply eq_eq_nat in e'. rewrite e' in e. discriminate.
Qed.
Definition eq_dec_term (n m : nat) : { n = m } + { n ≠ m } :=
match eq_nat n m as b return eq_nat n m = b → { n = m } + { n ≠ m } with
| true ⇒ fun (e : eq_nat n m = true) ⇒ left (eq_nat_eq n m e)
| false ⇒ fun (e : eq_nat n m = false) ⇒ right (eq_nat_false n m e)
end eq_refl.
Equivalences
There are many ways to define equivalences in Coq. We will choose one using
some notion of unique existence (∃!), defined below.
Then a function is an equivalence if there exists a unique antecedent to
each point.
exists_unique (fun x => P x) is to be read as "there exists a unique x such
that P x".
Definition exists_unique {A} (P : A → Prop) :=
{ x : A | P x ∧ ∀ y, P y → x = y }.
Definition isEquiv {X Y} (f : X → Y) :=
∀ y, exists_unique (fun x ⇒ y = f x).
Definition equivalence X Y :=
{ f : X → Y & isEquiv f }.
EXERCISE
Show that equivalences form an equivalence relation, that is that they are
reflexive, symmetric and transitive.
Next, show that nat is equivalent to nat*, ie nonzero natural numbers.
Hint: You can define this as a subset type (using {}) or nat.
Hint: You may need one extra axiom to complete the proof.
Lemma equivalence_refl X : equivalence X X.
Proof.
∃ (fun x ⇒ x).
intro y. ∃ y. split.
- reflexivity.
- intros x e. assumption.
Defined.
Lemma equivalence_sym :
∀ X Y,
equivalence X Y →
equivalence Y X.
Proof.
intros X Y [f h].
unshelve eexists.
- intro y. specialize (h y). destruct h as [x h]. exact x.
- intro x. ∃ (f x). split.
+ destruct (h (f x)) as [x' [e h']]. simpl.
symmetry. apply h'. reflexivity.
+ intros y e.
destruct (h y) as [x' [e' h']]. simpl in e.
subst. reflexivity.
Defined.
Lemma equivalence_trans :
∀ X Y Z,
equivalence X Y →
equivalence Y Z →
equivalence X Z.
Proof.
intros X Y Z [f hf] [g hg].
∃ (fun x ⇒ g (f x)).
intro z. specialize (hg z) as [y [e hy]]. subst.
specialize (hf y) as [x [e hx]]. subst.
∃ x. split.
- reflexivity.
- intros w e. apply hy in e. apply hx in e. assumption.
Qed.
Discriminating types
EXERCISE
Define a predicate on types that says that a type has exactly one inhabitant.
Deduce that unit is different from bool.
Next, show that nat is different from bool.
Definition all_equal A := ∀ (x y : A), x = y.
Lemma unit_neq_bool :
unit ≠ bool.
Proof.
intro e.
assert (h : all_equal unit).
{ intros [] []. reflexivity. }
rewrite e in h.
specialize (h true false). discriminate.
Qed.
Lemma nat_bool :
nat ≠ bool.
Proof.
pose (p X := ∀ x y z : X, x = y ∨ x = z ∨ y = z).
assert (p bool).
{ intros [] [] []; tauto. }
intros E. rewrite <- E in H.
specialize (H 0 1 2) as [ | []]; discriminate.
Qed.
(*** ADVANCED EXERCISES ***)
EXERCISE
Show extensionality of existential types.
In other words to prove that exist _ x hx = exist _ y hy, it is enough to
show x = y.
Hint: once again you may require an axiom to do it.
Lemma sig_ext :
∀ A (P : A → Prop) (x y : A) (hx : P x) (hy : P y),
x = y →
exist _ x hx = exist _ y hy.
Proof.
intros A P x y hx hy e.
destruct e. f_equal.
apply proof_irrelevance.
Qed.
EXERCISE
Show that bool ≠ unit using the shortest proof term you can find.
Definition unit_bool : bool ≠ unit.
refine (fun E ⇒
match eq_ind bool (fun X ⇒ ∃ x y : X, x ≠ y)
((ex_intro _ true (ex_intro _ false
(eq_ind true (fun b ⇒ if b then True else False) I _)))) _ E with
| ex_intro _ tt (ex_intro _ tt H2) ⇒ H2 eq_refl
end).
Defined.
EXERCISE
Until now, the equalities we considred have been *homogenous*, meaning
u = v requires both u and v to have the same type.
In some cases, it makes sense to compare two objects of a priori different
types. We can say that u : A and v : B are *heterogenously* equal when,
first A = B and then u = v up to a transport from A to B.
We can also define it inductively. Show that the two versions are equivalent.
Definition transport {A B} (e : A = B) (t : A) : B :=
match e with
| eq_refl ⇒ t
end.
Definition heq {A B} (u : A) (v : B) :=
{ e : A = B & transport e u = v }.
Inductive Heq {A} (u : A) : ∀ {B}, B → Prop :=
| heq_refl : Heq u u.
Lemma heq_Heq :
∀ A B (u : A) (v : B), heq u v → Heq u v.
Proof.
intros A B u v [e h].
destruct e. cbn in h. subst.
constructor.
Qed.
Lemma Heq_heq :
∀ A B (u : A) (v : B), Heq u v → heq u v.
Proof.
intros A B u v e.
destruct e.
∃ eq_refl. cbn. reflexivity.
Qed.
EXERCISE
Does heterogneous equality imply homogenous equality?
In other words can you prove the following?
∀ A (u v : A), Heq u v → u = v
Hint: Maybe it requires an axiom?
(* TODO *)
EXERCISE
Show that nat is equivalent to even natural numbers.
Lemma even_double :
∀ n, even (n × 2).
Proof.
intro n. induction n.
- constructor.
- simpl. constructor. assumption.
Qed.
Fixpoint div2 (n : nat) : nat :=
match n with
| 0 ⇒ 0
| 1 ⇒ 0
| S (S n) ⇒ S (div2 n)
end.
Lemma double_div2 :
∀ n,
even n →
div2 n × 2 = n.
Proof.
intros n h.
induction h.
- reflexivity.
- simpl. f_equal. f_equal. assumption.
Qed.
Lemma div2_double :
∀ n, div2 (n × 2) = n.
Proof.
intros n.
induction n.
- reflexivity.
- simpl. f_equal. assumption.
Qed.
Lemma equivalence_nat_even :
equivalence nat { n : nat | even n }.
Proof.
unshelve eexists (fun n ⇒ exist _ (n × 2) _).
{ simpl. apply even_double. }
intros [n h]. ∃ (div2 n). split.
- apply sig_ext. rewrite double_div2. 2: assumption.
reflexivity.
- intros m e. inversion e.
apply div2_double.
Qed.
EXERCISE
Cantor theorem for bool:
Show that there are no surjections from X to X -> bool.
In other words there are no f : X -> (X -> bool) such that
for all p there exists x such that f x = p.
Cantor theorem:
Show that there are no surjections from X to X -> Prop.
Now prove the following theorem:
Theorem Lawvere X Y :
∀ (f : X → (X → Y)),
(∀ g, ∃ x, f x = g) →
∀ (g : Y → Y), ∃ y, g y = y.
Proof.
intros f Hf g.
destruct (Hf (fun x ⇒ g (f x x))) as [x Hx].
∃ (f x x).
apply (f_equal (fun g ⇒ g x)) in Hx.
now rewrite <- Hx.
Qed.
EXERCISE
Can you get a simpler proof of the Cantor theorem for bool now?
Theorem Cantor_bool' X :
¬ ∃ f : X → (X → bool), ∀ p, ∃ x, f x = p.
Proof.
intros [f Hf].
apply Lawvere with (g := negb) in Hf as [y Hy].
destruct y; simpl in Hy; discriminate.
Qed.
J eliminator
We have seen eq_rect / eq_ind, but actually equality enjoys a stronger
induction principle called the J eliminator.
Instead of considering a predicate on an element, we also consider that the
predicate depends on an equality and that we only need to show it when the
equality is reflexivity to get it for all equalities.
Its type is the following. Show that you can indeed derive it.
Definition J :
∀ {A} {u : A} (P : ∀ z, u = z → Prop) {v : A} (t : P u eq_refl) (e : u = v),
P v e.
Proof.
intros A u P v t e.
destruct e. assumption.
Defined.
EXERCISE
We are now going to show that J is equivalent to singleton being contractible,
ie that singletons have a exactly one element.
For this we are going back to the world of Leibniz equality which does not
enjoy J.
You have to fill a few REPLACE_MEs but you should have solved them already
so you can easily copy paste your definitions, and all_equal should be
safely removed.
You can then prove the equivalence at the end of the module Leibniz2.
Module Leibniz2.
Definition leib_eq {A} (u v : A) :=
∀ (P : A → Prop), P u → P v.
Notation "u == v" := (leib_eq u v) (at level 80).
Definition refl {A} (a : A) : a == a :=
fun P (h : P a) ⇒ h.
Definition sym {A} (u v : A) (e : u == v) : v == u :=
fun P ⇒ e (fun x ⇒ P x → P u) (refl u P).
Lemma trans {A} (u v w : A) (e : u == v) (e' : v == w) : u == w.
Proof.
intro P.
apply e'. apply e.
Defined.
Definition J_prop :=
∀ A (u : A) (P : ∀ z, u == z → Prop) v (t : P u (refl u)) (e : u == v),
P v e.
Definition singleton {A} (x : A) := { y | x == y }.
Definition incl {A} (x : A) : singleton x :=
exist _ x (refl x).
Definition all_equal (A : Type) :=
∀ (x y : A), x == y.
Lemma all_equal_implies_J :
(∀ A (x : A), all_equal (singleton x)) →
J_prop.
Proof.
intro h. intros A u P v t e.
specialize (h _ u). specialize (h (incl u) (exist _ v e)).
specialize (h (fun '(exist _ x e) ⇒ P x e)).
simpl in h. apply h. assumption.
Qed.
Lemma all_equal_incl :
∀ A (x : A),
(∀ u, incl x == u) →
all_equal (singleton x).
Proof.
intros A x h. intros u v.
eapply trans.
- apply sym. apply h.
- apply h.
Qed.
Lemma J_implies_all_equal :
J_prop →
(∀ A (x : A), all_equal (singleton x)).
Proof.
intros J. intros A x.
apply all_equal_incl. intro u. intros P h.
destruct u as [y e].
specialize (J _ x (fun m p ⇒ P (exist _ m p))).
apply J. assumption.
Qed.
End Leibniz2.
EXERCISE
Uniqueness of identity proofs (UIP) is not provable in general but it still
holds for specific types, namely types with a decidable equality.
This fact is known as Hedberg's theorem.
We thus state UIP_for, so that UIP_for X means UIP holds for type X.
We're going first to prove UIP holds for nat.
Definition UIP_for X :=
∀ (u v : X) (p q : u = v), p = q.
Lemma nat_eqdec_eq x :
PeanoNat.Nat.eq_dec x x = left eq_refl.
Proof.
induction x. reflexivity.
simpl. rewrite IHx. reflexivity.
Qed.
Lemma UIP_nat' (x y: nat) :
∀ (e : x = y),
match PeanoNat.Nat.eq_dec x y with
| left e' ⇒ eq_ind _ _ eq_refl _ e' = e
| _ ⇒ True
end.
Proof.
destruct e. rewrite nat_eqdec_eq. reflexivity.
Qed.
Fact UIP_refl_nat (x: nat) :
∀ (e : x = x), e = eq_refl.
Proof.
intros e.
generalize (UIP_nat' x x e).
rewrite nat_eqdec_eq. cbv. intros []. reflexivity.
Qed.
Lemma UIP_for_nat : UIP_for nat.
Proof.
intros u v p q.
destruct q. apply UIP_refl_nat.
Qed.
EXERCISE
We are now going to prove the general case.
Prove Hedberg's theorem as follows.
Definition HF X (f : ∀ (x y : X), x = y → x = y) :=
∀ x y (e e' : x = y), f x y e = f x y e'.
Lemma Hedberg' X :
ex (HF X) → UIP_for X.
Proof.
intros [f H] x y.
enough (∀ e: x = y, eq_trans (f x y e) (eq_sym (f y y eq_refl)) = e) as H1.
- intros e e'. specialize (H _ _ e e'). congruence.
- destruct e. cbv. destruct f; reflexivity.
Qed.
Theorem Hedberg X :
(∀ x y: X, x = y ∨ x ≠ y) → UIP_for X.
Proof.
intros d. apply Hedberg'.
∃ (fun x y e ⇒ match d x y with or_introl e' ⇒ e' | _ ⇒ e end).
intros x y e e'.
destruct d as [e''|h].
- reflexivity.
- exfalso. exact (h e).
Qed.
EXERCISE
FunExt as stated above is not general enough. Indeed, functions can be
dependent so in practice we use the following axiom for function
extensionality.
Using it, we can show that two functions of type nat -> bool are equal if and
only if they are not not equal. Prove it.
Definition FunctionExtensionality :=
∀ A B, ∀ (f g : ∀ (x : A), B x), (∀ x, f x = g x) → f = g.
Definition stable (P : Prop) :=
~~P → P.
Fact FE_stable_HF X :
FunctionExtensionality →
(∀ (x y : X), stable (x = y)) →
sig (HF X).
Proof.
intros F G.
∃ (fun x y e ⇒ G x y (fun f ⇒ match f e with end)).
intros x y e e'. f_equal. apply F. intros f.
exfalso. exact (f e).
Qed.
Fact FE_test_eq_stable :
FunctionExtensionality →
∀ (f g : nat → bool), stable (f = g).
Proof.
intros F f g H. apply F. intros x.
destruct (f x) eqn:E1, (g x) eqn:E2.
- reflexivity.
- contradict H. intros →. contradict E1. rewrite E2. discriminate.
- contradict H. intros →. contradict E1. rewrite E2. discriminate.
- reflexivity.
Qed.
EXERCISE
You may or may not have heard of homotopy type theory and univalent
foundations. This is a relatively recent development in which equality of
types corresponds to equivalences. This essentially justifies the informal
mathematical practice of considering isomorphic objects to be the same.
Define a term to_equiv that inhabits equivalence X Y from X = Y.
Univalence is then stated as this function being itself being an equivalence.
Definition to_equiv X Y : X = Y → equivalence X Y.
Proof.
intro e. destruct e. apply equivalence_refl.
Defined.
Definition Univalence :=
∀ (X Y : Type), isEquiv (to_equiv X Y).
EXERCISE
Show that assuming univalence, equivalent types are equal.
Lemma univalence_equiv_equal :
Univalence →
(∀ X Y, equivalence X Y → X = Y).
Proof.
intros uni X Y h.
assert (h' : equivalence (X = Y) (equivalence X Y)).
{ ∃ (to_equiv X Y). apply uni. }
apply equivalence_sym in h'.
destruct h' as [f h'].
apply f. assumption.
Qed.
EXERCISE
Univalence is incompatible with UIP. One way is to show that there are two
ways to prove bool = bool, so that by univalence (bool = bool) is itself equal
to type bool.
Show that there exists another equivalence than identity between bool and
itself.
Deducing equivalence bool (equivalence bool bool) should now be possible but
it is quite hard so don't waste to much energy on it.
Alternatively you can use the following lemma to deduce that Univalence
negates UIP.
Lemma SIP_UIP :
@existT Set (fun X ⇒ X) bool true = @existT Set (fun X ⇒ X) bool false →
∃ (p : bool = bool), p ≠ eq_refl.
Proof.
intros H. ∃ (projT1_eq H). intros H'.
specialize (projT2_eq H). rewrite H'.
cbn. discriminate.
Qed.
Definition equivalence_neg_bool : equivalence bool bool.
Proof.
∃ negb.
intro b. ∃ (negb b). split.
- destruct b. all: reflexivity.
- intros b' e. destruct b, b'. all: try discriminate. all: reflexivity.
Defined.
Lemma equivalence_eq_eq :
∀ A B,
Univalence →
equivalence A B = (A = B).
Proof.
intros A B uni.
symmetry. apply univalence_equiv_equal. 1: assumption.
∃ (to_equiv A B).
apply uni.
Qed.
Lemma Univalence_neg_UIP :
Univalence → ¬ UIP.
Proof.
intros uni uip.
pose proof (equivalence_eq_eq bool bool uni) as e.
assert (h : ∀ p q : equivalence bool bool, p = q).
{ rewrite e. intros. apply uip. }
specialize (h (equivalence_refl bool) equivalence_neg_bool).
inversion h.
apply (f_equal (fun x ⇒ x true)) in H0.
simpl in H0. discriminate.
Qed.