The file 'curry.v' as Latin-1 characters
1 ( * ␣ h t t p s : / / w w w . y o u t u b e . c o m / w a t c h ? v = i 2 Q 5 G J h g s j A ␣ * ) EOL()
2 ( * ␣ h t t p s : / / w w w . y o u t u b e . c o m / w a t c h ? v = 2 S j M 5 f 3 G k V 0 ␣ * ) EOL()
3 ( * ␣ h t t p : / / m a t h . a n d r e j . c o m / 2 0 1 1 / 0 2 / 2 2 / v i d e o - t u t o r i a l s - f o r - t h e - c o q - p r o o f - a s s i s t a n t / ␣ * ) EOL()
4 EOL()
5 P a r a m e t e r s ␣ A ␣ B ␣ C ␣ : ␣ S e t . EOL()
6 EOL()
7 ( * ␣ A ␣ f u n c t i o n ␣ f ␣ : ␣ A ␣ * ␣ B ␣ - > ␣ C ␣ i s ␣ e q u i v a l e n t ␣ t o ␣ a ␣ f u n c t i o n ␣ A ␣ - > ␣ ( B ␣ - > ␣ C ) . ␣ * ) EOL()
8 D e f i n i t i o n ␣ c u r r y ␣ ␣ ␣ ( f ␣ : ␣ A ␣ * ␣ B ␣ - > ␣ C ) ␣ : = ␣ f u n ␣ a ␣ = > ␣ f u n ␣ b ␣ = > ␣ f ␣ ( a , ␣ b ) . EOL()
9 D e f i n i t i o n ␣ u n c u r r y ␣ ( g ␣ : ␣ A ␣ - > ␣ B ␣ - > ␣ C ) ␣ : = ␣ f u n ␣ p ␣ = > ␣ g ␣ ( f s t ␣ p ) ␣ ( s n d ␣ p ) . EOL()
10 EOL()
11 ( * ␣ " e x t e n s i o n a l ␣ e q u a l i t y " ␣ * ) EOL()
12 T h e o r e m ␣ L e f t _ I n v e r s e ␣ : ␣ f o r a l l ␣ f ␣ a ␣ b , ␣ u n c u r r y ␣ ( c u r r y ␣ f ) ␣ ( a , ␣ b ) ␣ = ␣ f ␣ ( a , ␣ b ) . EOL()
13 P r o o f . EOL()
14 ␣ ␣ i n t r o s . EOL()
15 ␣ ␣ u n f o l d ␣ c u r r y , ␣ u n c u r r y . EOL()
16 ␣ ␣ s i m p l . EOL()
17 ␣ ␣ r e f l e x i v i t y . EOL()
18 Q e d . EOL()
19 EOL()
20 ( * ␣ P r o v e ␣ t h a t ␣ c u r r y ␣ ( u n c u r r y ␣ g ) ␣ i s ␣ e x t e n s i o n a l l y ␣ e q u i v a l e n t ␣ t o ␣ g . ␣ * ) EOL()
21 T h e o r e m ␣ R i g h t _ I n v e r s e ␣ : ␣ f o r a l l ␣ g ␣ a ␣ b , ␣ c u r r y ␣ ( u n c u r r y ␣ g ) ␣ a ␣ b ␣ = ␣ g ␣ a ␣ b . EOL()
22 P r o o f . EOL()
23 ␣ ␣ i n t r o s . EOL()
24 ␣ ␣ u n f o l d ␣ c u r r y , ␣ u n c u r r y . EOL()
25 ␣ ␣ s i m p l . EOL()
26 ␣ ␣ r e f l e x i v i t y . EOL()
27 Q e d . EOL()
28 EOL()
29 ( * ␣ T h e r e ␣ e x i s t ␣ b i j e c t i o n s ␣ b a c k ␣ a n d ␣ f o r t h . ␣ * ) EOL()
30 D e f i n i t i o n ␣ I s o m o r p h i c ␣ ( X ␣ Y ␣ : ␣ S e t ) ␣ : = EOL()
31 ␣ ␣ e x i s t s ␣ f ␣ : ␣ X ␣ - > ␣ Y , EOL()
32 ␣ ␣ ␣ ␣ e x i s t s ␣ g ␣ : ␣ Y ␣ - > ␣ X , EOL()
33 ␣ ␣ ␣ ␣ ␣ ␣ ( f o r a l l ␣ x , ␣ g ( f ( x ) ) ␣ = ␣ x ␣ / \ ␣ ( f o r a l l ␣ y , ␣ f ( g ( y ) ) ␣ = ␣ y ) ) . EOL()
34 EOL()
35 A x i o m ␣ E x t e n s i o n a l i t y ␣ : ␣ f o r a l l ␣ ( X ␣ Y ␣ : ␣ S e t ) ␣ ( f ␣ g ␣ : ␣ X ␣ - > ␣ Y ) , EOL()
36 ␣ ␣ ( f o r a l l ␣ x , ␣ f ␣ x ␣ = ␣ g ␣ x ) ␣ - > ␣ f ␣ = ␣ g . EOL()
37 EOL()
38 ( * ␣ W h e n ␣ y o u ␣ s e e ␣ y o u r ␣ g o a l ␣ i s ␣ g o i n g ␣ t o ␣ f a l l ␣ a p a r t ␣ i n t o ␣ s e v e r a l ␣ c a s e s , EOL()
39 ␣ ␣ ` s p l i t ` ␣ i s ␣ u s u a l l y ␣ t h e ␣ p r o p e r ␣ t a c t i c . ␣ * ) EOL()
40 T h e o r e m ␣ I s o F u n S p a c e ␣ : ␣ I s o m o r p h i c ␣ ( A ␣ * ␣ B ␣ - > ␣ C ) ␣ ( A ␣ - > ␣ B ␣ - > ␣ C ) . EOL()
41 P r o o f . EOL()
42 ␣ ␣ e x i s t s ␣ c u r r y , ␣ u n c u r r y . EOL()
43 ␣ ␣ s p l i t . EOL()
44 ␣ ␣ a p p l y ␣ E x t e n s i o n a l i t y . ␣ ␣ i n t r o s ␣ [ a ␣ b ] . EOL()
45 ␣ ␣ a p p l y ␣ L e f t _ I n v e r s e . ␣ ␣ i n t r o ␣ g . EOL()
46 ␣ ␣ a p p l y ␣ E x t e n s i o n a l i t y . ␣ ␣ i n t r o ␣ a . EOL()
47 ␣ ␣ a p p l y ␣ E x t e n s i o n a l i t y . ␣ ␣ i n t r o ␣ b . EOL()
48 ␣ ␣ a p p l y ␣ R i g h t _ I n v e r s e . EOL()
49 Q e d . EOL()