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:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e. #A #B * // qed. lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C. R (P (\fst x) (\snd 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. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. #A #B #a1 #a2 #b1 #b2 #H destruct // qed. lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. #A #B #a1 #a2 #b1 #b2 #H destruct // qed.