aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
blob: f65d733388132c1c3e33e63430405e640b022ad7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
(** * The Structure of the [eq] Type *)
(** As described by the project of homotopy type theory, there is a
    lot of structure inherent in the type of propositional equality,
    [eq].  We build up enough lemmas about this structure to deal
    nicely with proofs of equality that come up in practice in this
    project. *)
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Isomorphism.
Require Import Crypto.Util.HProp.

Import EqNotations.

Definition f_equal_dep {A B} (f : forall a : A, B a) (x y : A) (H : x = y) : rew [B] H in f x = f y
  := match H with
     | eq_refl => eq_refl
     end.

(** Most of the structure of proofs of equalities fits into what
    mathematicians call a weak ∞-groupoid.  (In fact, one way of
    *defining* a weak ∞-groupoid is via what's called the J-rule,
    which exactly matches the eliminator [eq_rect] for the equality
    type [eq].)  The first level of this groupoid is given by the
    identity [eq_refl], the binary operation [eq_trans], and the
    inverse of [p : x = y] given by [eq_sym p : y = x].  The second
    level, which we provide here, says that [id ∘ p = p = p ∘ id],
    that [(p ∘ q)⁻¹ = q⁻¹ ∘ p⁻¹], that [(p⁻¹)⁻¹ = p], and that [p ∘
    p⁻¹ = p⁻¹ ∘ p = id].  We prove these here, as well as a few lemmas
    about functoriality of functions over equality. *)
Definition concat_1p {A x y} (p : x = y :> A) : eq_trans eq_refl p = p.
Proof. case p; reflexivity. Defined.
Definition concat_p1 {A x y} (p : x = y :> A) : eq_trans p eq_refl = p.
Proof. case p; reflexivity. Defined.
Definition concat_pV {A x y} (p : x = y :> A) : eq_trans p (eq_sym p) = eq_refl.
Proof. case p; reflexivity. Defined.
Definition concat_Vp {A x y} (p : x = y :> A) : eq_trans (eq_sym p) p = eq_refl.
Proof. case p; reflexivity. Defined.
Definition transport_pp {A} {P : A -> Type} {x y z} (p : x = y) (q : y = z) (k : P x)
: eq_rect _ P k _ (eq_trans p q) = eq_rect _ P (eq_rect _ P k _ p) _ q.
Proof. case q; simpl; reflexivity. Defined.
Lemma transport_const {A P x y} (p : x = y :> A) k
: eq_rect _ (fun _ : A => P) k _ p = k.
Proof. case p; reflexivity. Defined.
Lemma ap_const {A B x y} (b : B) (p : x = y :> A)
: f_equal (fun _ => b) p = eq_refl.
Proof. case p; reflexivity. Defined.
Lemma inv_pp {A x y z} (p : x = y :> A) (q : y = z :> A)
: eq_sym (eq_trans p q) = eq_trans (eq_sym q) (eq_sym p).
Proof. case q; case p; reflexivity. Defined.
Lemma inv_V {A x y} (p : x = y :> A)
: eq_sym (eq_sym p) = p.
Proof. case p; reflexivity. Defined.
Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
  : eq_rect _ P u _ p = eq_rect _ (fun T => T) u _ (f_equal P p).
Proof. case p; reflexivity. Defined.
Definition ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x)
  : f _ (@eq_rect A x P z y p) = @eq_rect A x Q (f _ z) y p.
Proof. case p; reflexivity. Defined.

(** To classify the equalities of a type [A] at a point [a : A], we
    must give a "code" that stands in for the type [a = x] for each
    [x], and a way of "encoding" proofs of equality into the code that
    we claim represents this type.  To prove that the code is good, it
    turns out that it sufficies to prove that it is freely generated
    by the encoding of [eq_refl], i.e., that [{ x : A & a = x }] and
    [{ x : A & code x }] are equivalent, i.e., that [{ x : A & code x
    }] is an hProp (has at most one element).  When this is the case,
    we have fully classified the type of equalities in [A] at [a] up
    to isomorphism.  This lets us replace proofs of equalities in [A]
    with their codes, which are frequently easier to manipulate.  (For
    example, the code for [x = y :> A * B] is [(fst x = fst y) * (snd
    x = snd y)], whence we can destruct the pair.)

    This method of proof, introduced in homotopy type theory, is
    called encode-decode. *)
Section gen.
  Context {A : Type} {x : A} (code : A -> Type)
          (encode : forall y, x = y -> code y)
          {code_hprop : IsHProp { a : A & code a } }.

  Definition decode' {y} (p : code y) : x = y
    := f_equal (@projT1 _ _) (code_hprop (existT _ x (encode x eq_refl)) (existT _ y p)).

  Definition decode {y} (H : code y) : x = y
    := eq_trans (eq_sym (decode' (encode x eq_refl))) (decode' H).

  Definition deencode {y} (H : x = y) : decode (encode y H) = H.
  Proof.
    destruct H.
    unfold decode.
    edestruct (decode' (encode x eq_refl)).
    reflexivity.
  Defined.

  Global Instance isiso_encode : forall {y}, IsIso (encode y).
  Proof.
    intro y.
    exists (@decode y).
    { intro H.
      unfold decode.
      set (yH := (existT _ y H)).
      change H with (projT2 yH).
      change y with (projT1 yH).
      clearbody yH; clear y H.
      destruct (code_hprop (existT _ x (encode x eq_refl)) yH); simpl.
      abstract (rewrite concat_Vp; reflexivity). }
    { intro p.
      apply deencode. }
  Defined.
End gen.

(** We use the encode-decode method to prove that if [forall x y : A,
    x = y], then [forall (x y : A) (p q : x = y), p = q]. *)
(* It's not clear whether this should be in this file, or in HProp.
   But we require [IsHProp] above, so we leave it here for now. *)
Section hprop.
  Context {A} `{IsHProp A}.

  Let hprop_encode {x y : A} (p : x = y) : unit := tt.

  Local Hint Resolve (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.

  Global Instance ishprop_path_hprop : IsHPropRel (@eq A).
  Proof.
    intros x y p q.
    pose proof (is_left_inv (@hprop_encode x y)) as H'.
    rewrite <- (H' p), <- (H' q).
    apply f_equal; apply allpath_hprop.
  Qed.
End hprop.


Lemma commute_eq_rect {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H : a = b :> A)
      (v : P a)
  : f b (eq_rect _ P v _ H)
    = eq_rect _ Q (f a v) _ H.
Proof. destruct H; reflexivity. Defined.

Lemma commute_eq_match {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H : a = b :> A)
      (v : P a)
  : f b (match H in _ = y return P y with eq_refl => v end)
    = (match H in _ = y return Q y with eq_refl => f a v end).
Proof. destruct H; reflexivity. Defined.
Lemma commute_eq_match2 {A} (P1 P2 Q : A -> Type) (f : forall a, P1 a -> P2 a -> Q a) a b (H : a = b :> A)
      (v1 : P1 a) (v2 : P2 a)
  : f b
      (match H in _ = y return P1 y with eq_refl => v1 end)
      (match H in _ = y return P2 y with eq_refl => v2 end)
    = (match H in _ = y return Q y with eq_refl => f a v1 v2 end).
Proof. destruct H; reflexivity. Defined.
Lemma eq_match_const {A P x y} (p : x = y :> A) k
  : match p return P with eq_refl => k end = k.
Proof. case p; reflexivity. Defined.

Lemma fg_equal {A B} (f g : A -> B) (x y : A)
  : f = g -> x = y -> f x = g y.
Proof. intros; subst; reflexivity. Defined.

Lemma fg_equal_rel {A B R} (f g : A -> B) (x y : A)
  : (pointwise_relation _ R) f g -> x = y -> R (f x) (g y).
Proof. cbv [pointwise_relation]; intros; subst; trivial. Qed.

Lemma push_rew_fun_dep A P Q a b (pf : a = b) f x
  : (rew [fun x : A => P x -> Q x] pf in f) x = (rew [Q] pf in (f (rew <- [P] pf in x))).
Proof. subst; reflexivity. Defined.

Lemma rew_r_moveL A P x y (pf : x = y :> A) a b
  : (rew [P] pf in a) = b -> a = (rew <- [P] pf in b).
Proof. subst; exact id. Defined.
Lemma rew_moveL A P x y (pf : x = y :> A) a b
  : (rew <- [P] pf in a) = b -> a = (rew [P] pf in b).
Proof. subst; exact id. Defined.

Lemma rew_moveR A P x y (pf : x = y :> A) a b
  : a = (rew <- [P] pf in b) -> (rew [P] pf in a) = b.
Proof. subst; exact id. Defined.
Lemma rew_r_moveR A P x y (pf : x = y :> A) a b
  : a = (rew [P] pf in b) -> (rew <- [P] pf in a) = b.
Proof. subst; exact id. Defined.