weblib/Cerco/utilities/pair.ma

   1 include "basics/types.ma".
   2
   3 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
   4  with precedence 10
   5 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
   6
   7 (* Also extracts an equality proof (useful when not using Russell). *)
   8 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
   9  with precedence 10
  10 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
  11         λ${ident E}.$s ] (refl ? $t) }.
  12
  13 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
  14  with precedence 10
  15 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
  16        match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
  17         λ${ident E}.$s ] ] (refl ? $t) }.
  18
  19 (* This appears to upset automation (previously provable results require greater
  20    depth or just don't work), so use example rather than lemma to prevent it
  21    being indexed. *)
  22 example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
  23 #A #B * // qed.
  24
  25 lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
  26 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
  27 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
  28 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
  29
  30 lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
  31   R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
  32 #A #B #C *; normalize /2/
  33 qed.
  34
  35 notation "π1" with precedence 10 for @{ (proj1 ??) }.
  36 notation "π2" with precedence 10 for @{ (proj2 ??) }.
  37
  38 (* Useful for avoiding destruct's full normalization. *)
  39 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
  40 #A #B #a1 #a2 #b1 #b2 #H destruct //
  41 qed.
  42
  43 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
  44 #A #B #a1 #a2 #b1 #b2 #H destruct //
  45 qed.