feat(library/standard): add piext axiom, and theorems that follow from it

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/cast.lean

@@ -20,6 +20,9 @@ definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
 
 infixl `==`:50 := heq
 
+theorem heq_elim {A B : Type} {C : Bool} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C
+:= obtain w Hw, from H1, H2 w Hw
+
 theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
 := obtain w Hw, from H, w
 
@@ -62,6 +65,9 @@ calc_trans htrans
 calc_trans htrans_left
 calc_trans htrans_right
 
+theorem type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
+:= hsubst H (refl A)
+
 theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a
 := have H1 : ∀ (H : A = A) (a : A), cast H a == a, from
      λ H a, eq_to_heq (cast_eq H a),

library/standard/piext.lean

@@ -0,0 +1,34 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import logic cast
+
+-- Pi extensionality
+axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : (Π x, B x) = (Π x, B' x) → B = B'
+
+theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a
+:= have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
+   have Hb : B = B', from piext H,
+   have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
+     assume H, eq_to_heq (congr1 (cast_eq H f) a),
+   have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
+     subst Hb H1,
+   H2 H
+
+theorem cast_pull {A : Type} {B B' : A → Type} (f : Π x, B x) (a : A) (Hb : (Π x, B x) = (Π x, B' x)) (Hba : (B a) = (B' a)) :
+                  cast Hb f a = cast Hba (f a)
+:= heq_to_eq (calc cast Hb f a == f a            : cast_app Hb f a
+                         ...   == cast Hba (f a) : hsymm (cast_heq Hba (f a)))
+
+theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a
+:= heq_elim H (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
+     calc f a == cast Ht f a  : hsymm (cast_app Ht f a)
+          ... =  f' a         : congr1 Hw a)
+
+theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
+               (Hff' : f == f') (Haa' : a == a') : f a == f' a'
+:= have H : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
+     take B B' f f' e, hcongr1 a e,
+   @hsubst _ _ _ _ (fun (X : Type) (x : X),
+       ∀ (B : A → Type) (B' : X → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' x)
+       Haa' H B B' f f' Hff'