include "basics/types.ma".

notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
 with precedence 10
for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.

(* Also extracts an equality proof (useful when not using Russell). *)
notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
        λ${ident E}.$s ] (refl ? $t) }.

notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
       match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
        λ${ident E}.$s ] ] (refl ? $t) }.

(* This appears to upset automation (previously provable results require greater
   depth or just don't work), so use example rather than lemma to prevent it
   being indexed. *)
example contract_pair : ∀A,B.∀e:AA title="Product" href="cic:/fakeuri.def(1)"×/AB. (let 〈a,b〉 ≝ e in A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa,b〉) A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A e.
#A #B * // qed.

lemma extract_pair : ∀A,B,C,D.  ∀u:AA title="Product" href="cic:/fakeuri.def(1)"×/AB. ∀Q:A → B → CA title="Product" href="cic:/fakeuri.def(1)"×/AD. ∀x,y.
((let 〈a,b〉 ≝ u in Q a b) A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Ax,y〉) →
A title="exists" href="cic:/fakeuri.def(1)"∃/Aa,b. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa,b〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A u A title="logical and" href="cic:/fakeuri.def(1)"∧/A Q a b A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Ax,y〉.
#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A @E1 qed.

lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
  R (P (A title="pair pi1" href="cic:/fakeuri.def(1)"\fst/A x) (A title="pair pi2" href="cic:/fakeuri.def(1)"\snd/A x)) → R (let 〈a,b〉 ≝ x in P a b).
#A #B #C *; normalize /2/
qed.

notation "π1" with precedence 10 for @{ (proj1 ??) }.
notation "π2" with precedence 10 for @{ (proj2 ??) }.

(* Useful for avoiding destruct's full normalization. *)
lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa1,b1〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa2,b2〉 → a1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a2.
#A #B #a1 #a2 #b1 #b2 #H destruct //
qed.

lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa1,b1〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa2,b2〉 → b1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b2.
#A #B #a1 #a2 #b1 #b2 #H destruct //
qed.