some injection instances for poption.

Author: gmalecha

theories/Data/POption.v

@@ -1,5 +1,6 @@
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
+Require Import ExtLib.Tactics.Injection.
 
 Set Printing Universes.
 
@@ -11,6 +12,45 @@ Section poption.
   | pSome : T -> poption
   | pNone.
 
+  Global Polymorphic Instance Injective_pSome a b
+  : Injective (pSome a = pSome b) :=
+  { result := a = b
+  ; injection := fun pf =>
+                   match pf in _ = X
+                         return a = match X with
+                                    | pSome y => y
+                                    | _ => a
+                                    end
+                   with
+                   | eq_refl => eq_refl
+                   end }.
+
+  Global Polymorphic Instance Injective_pSome_pNone a
+  : Injective (pSome a = pNone) :=
+  { result := False
+  ; injection := fun pf =>
+                   match pf in _ = X
+                         return match X with
+                                | pSome y => True
+                                | _ => False
+                                end
+                   with
+                   | eq_refl => I
+                   end }.
+
+  Global Polymorphic Instance Injective_pNone_pSome a
+  : Injective (pNone = pSome a) :=
+  { result := False
+  ; injection := fun pf =>
+                   match pf in _ = X
+                         return match X with
+                                | pNone => True
+                                | _ => False
+                                end
+                   with
+                   | eq_refl => I
+                   end }.
+
 End poption.
 
 Arguments pSome {_} _.
@@ -45,4 +85,4 @@ Existing Instance Functor_poption.
 Polymorphic Definition Applicative_poption@{i} : Applicative@{i i} poption@{i} :=
 {| pure := @pSome@{i}
  ; ap   := @ap_poption |}.
-Existing Instance Applicative_poption.
+Existing Instance Applicative_poption.