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 [ mk_Prod ${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 [ mk_Prod ${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 [ mk_Prod ${fresh xy} ${ident z} ⇒ |
---|

16 | match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${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. |
---|