coercible (#121)

affeldt-aist · Aug 5, 2023 · 9695399 · 9695399
1 parent 076edc2
commit 9695399
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 34 deletions.
diff --git a/monad_model.v b/monad_model.v
@@ -1731,15 +1731,15 @@ Variant nth_error_spec (T : ml_type) (e : Env) (r : loc T) : Type :=
   | NthError : forall s : coq_type M T,
     nth_error e (loc_id r) = Some (mkbind T s) -> nth_error_spec e r
   | NthError_nocoerce : forall T' (s' : coq_type M T'),
-    nth_error e (loc_id r) = Some (mkbind T' s') -> ~ coerce T s' ->
+    nth_error e (loc_id r) = Some (mkbind T' s') -> ~~ coercible T s' ->
     nth_error_spec e r
   | NthError_None : nth_error e (loc_id r) = None -> nth_error_spec e r.
 
 Lemma ntherrorP (T : ml_type) (e : Env) (r : loc T) : nth_error_spec e r.
 Proof.
 case H : (nth_error e (loc_id r)) => [[T' s']|].
-  have [Ts'|Ts'] := boolp.pselect (coerce T s').
-    have ? := coerce_eq Ts'; subst T'.
+  have [Ts'|Ts'] := boolP (coercible T s').
+    have ? := coercible_eq Ts'; subst T'.
     exact: NthError H.
   exact: NthError_nocoerce H Ts'.
 exact: NthError_None.
@@ -1772,19 +1772,17 @@ Qed.
 
 Lemma nocoerce_cget T (r : loc T) T' (s' : coq_type M T') e :
   nth_error e (loc_id r) = Some (mkbind T' s') ->
-  ~ coerce T s' ->
+  ~~ coercible T s' ->
   cget r e = fail.
-Proof. by move=> H Ts'; rewrite /cget H; case: coerce Ts'. Qed.
+Proof. by move=> H Ts'; rewrite /cget H not_coercible. Qed.
 
 Lemma nocoerce_cput T (r : loc T) (s : coq_type M T) (T' : ml_type)
     (s' : coq_type M T') e :
   nth_error e (loc_id r) = Some (mkbind T' s') ->
-  ~ coerce T s' ->
+  ~~ coercible T s' ->
   cput r s e = fail.
 Proof.
-move=> H Ts'; rewrite /cput H.
-have {}Ts' : ~ coerce T' s by apply: contra_not Ts'; exact: coerce_sym.
-by case: coerce Ts'.
+by move=> H Ts'; rewrite /cput H not_coercible// (coercible_sym _ s').
 Qed.
 
 Lemma None_cget T (r : loc T) e :
@@ -1808,9 +1806,7 @@ Qed.
 Lemma Some_cput T (r : loc T) (s : coq_type M T) e :
   nth_error e (loc_id r) = Some (mkbind T s) ->
   cput r s e = (@skip M) e.
-Proof.
-by move=> H; rewrite /cput/= H coerce_Some/= nth_error_set_nth_id.
-Qed.
+Proof. by move=> H; rewrite /cput/= H coerce_Some/= nth_error_set_nth_id. Qed.
 
 Let cgetputskip T (r : loc T) : cget r >>= cput r = cget r >> skip.
 Proof.
@@ -1988,7 +1984,7 @@ Lemma cput_then_fail T1 T2 T1' e (s1' : coq_type M T1')
     (r2 : loc T2) (s2 : coq_type M T2)
     (r1 : loc T1) (s1 : coq_type M T1) :
   nth_error e (loc_id r1) = Some (mkbind T1' s1') ->
-  ~ coerce T1 s1' ->
+  ~~ coercible T1 s1' ->
   (cput r2 s2 >> cput r1 s1) e = fail.
 Proof.
 move=> Hr1 T1s'.
@@ -2003,7 +1999,7 @@ have [v Hr2|T2' v Hr2 T2v|Hr2] := ntherrorP e r2; last first.
     subst T2.
     rewrite coerce_Some//=.
     move: Hr1; rewrite Hr Hr2 => -[?]; subst T1' => _.
-    by rewrite coerce_Some // in T1s'.
+    by rewrite coercible_Some // in T1s'.
   + rewrite (nocoerce_cput _ _ T1s')//=.
     by rewrite (@nth_error_set_nth_other _ _ _ _ _ (mkbind T1' s1')).
 Qed.
@@ -2072,7 +2068,7 @@ have [u Hr1|T1' s1' Hr1 T1s'|Hr1] := ntherrorP e r1.
   + rewrite [RHS]MS_bindE (nocoerce_cget _ T2s')// bindfailf.
     rewrite !MS_bindE /cput Hr1 coerce_Some bindretf//=.
     rewrite MS_bindE /cget/= (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym//.
-    by move: (T2s'); case: coerce.
+    by rewrite not_coercible.
   + rewrite [in RHS]MS_bindE None_cget// bindfailf.
     rewrite MS_bindE /cput Hr1 coerce_Some bindretf/=.
     by rewrite MS_bindE /cget (nth_error_set_nth_none _ _ Hr2 Hr1).

diff --git a/monae_lib.v b/monae_lib.v
@@ -229,20 +229,39 @@ Variables (X : eqType) (f : X -> Type).
 Definition coerce (T1 T2 : X) (v : f T1) : option (f T2) :=
   if @eqPc _ T1 T2 is ReflectT H then Some (eq_rect _ _ v _ H) else None.
 
-Lemma coerce_sym (T T' : X) (s : f T) (s' : f T') : coerce T' s -> coerce T s'.
-Proof.
-by rewrite /coerce; case: eqPc => //= h; case: eqPc => //; rewrite h; auto.
-Qed.
-
 Lemma coerce_Some (T : X) (s : f T) : coerce T s = Some s.
 Proof.
 by rewrite /coerce; case: eqPc => /= [?|]; [rewrite -eq_rect_eq|auto].
 Qed.
 
-Lemma coerce_eq (T T' : X) (s : f T) : coerce T' s -> T = T'.
-Proof. by rewrite /coerce; case: eqPc. Qed.
-
 Lemma coerce_None (T T' : X) (s : f T) : T != T' -> coerce T' s = None.
 Proof. by rewrite /coerce; case: eqPc. Qed.
 
+Lemma coerce_sym (T T' : X) (s : f T) (s' : f T') :
+  coerce T' s = Some s' -> coerce T s' = Some s.
+Proof.
+rewrite /coerce; case: eqPc => //= h; case: eqPc => //.
+  by move=> h'/= [<-]; subst T'; rewrite -!eq_rect_eq.
+by rewrite {1}h; auto.
+Qed.
+
+Definition coercible (T1 T2 : X) (v : f T1) : bool := coerce T2 v.
+
+Lemma coercible_Some (T : X) (s : f T) : coercible T s.
+Proof. by rewrite /coercible coerce_Some. Qed.
+
+Lemma not_coercible (T T' : X) (s : f T) : ~~ coercible T' s -> coerce T' s = None.
+Proof. by rewrite /coercible; case: (coerce _). Qed.
+
+Lemma coercible_eq (T T' : X) (s : f T) : coercible T' s -> T = T'.
+Proof. by rewrite /coercible; apply: boolp.contraPP => /eqP/coerce_None ->. Qed.
+
+Lemma coercible_sym (T T' : X) (s : f T) (s' : f T') :
+  coercible T' s = coercible T s'.
+Proof.
+rewrite /coercible /coerce; case: eqPc; case: eqPc => //.
+- by move=> ? ?; subst T'; rewrite -!eq_rect_eq.
+- by move=> ? ?; exfalso; auto.
+Qed.
+
 End coerce.
diff --git a/typed_store_model.v b/typed_store_model.v
@@ -102,9 +102,9 @@ Arguments Some_cget {T r} s.
 
 Lemma nocoerce_cget T (r : loc T) T' (s' : coq_type T') e :
   nth_error (ofEnv e) (loc_id r) = Some (mkbind s') ->
-  ~ coerce T s' ->
+  ~~ coercible T s' ->
   cget r e = fail.
-Proof. by move=> H Ts'; rewrite /cget H; case: coerce Ts'. Qed.
+Proof. by move=> H Ts'; rewrite /cget H not_coercible. Qed.
 
 Lemma None_cget T (r : loc T) e :
   nth_error (ofEnv e) (loc_id r) = None ->
@@ -121,12 +121,11 @@ Qed.
 
 Lemma nocoerce_cput T (r : loc T) (s : coq_type T) T' (s' : coq_type T') e :
   nth_error (ofEnv e) (loc_id r) = Some (mkbind s') ->
-  ~ coerce T s' ->
+  ~~ coercible T s' ->
   cput r s e = fail.
 Proof.
 move=> H Ts'; move: e H => [e] H; rewrite /cput H.
-have {}Ts' : ~ coerce T' s by apply: contra_not Ts'; exact: coerce_sym.
-by case: coerce Ts'.
+by rewrite not_coercible// (coercible_sym _ s').
 Qed.
 
 Lemma None_cput T (r : loc T) (s : coq_type T) e :
@@ -166,15 +165,15 @@ Variant nth_error_spec (T : MLU) (e : Env) (r : loc T) : Type :=
   | NthError : forall s : coq_type T,
     nth_error (ofEnv e) (loc_id r) = Some (mkbind s) -> nth_error_spec e r
   | NthError_nocoerce : forall T' (s' : coq_type T'),
-    nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> ~ coerce T s' ->
+    nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> ~~ coercible T s' ->
     nth_error_spec e r
   | NthError_None : nth_error (ofEnv e) (loc_id r) = None -> nth_error_spec e r.
 
 Lemma ntherrorP (T : MLU) (e : Env) (r : loc T) : nth_error_spec e r.
 Proof.
 case H : (nth_error (ofEnv e) (loc_id r)) => [[T' s']|].
-  have [Ts'|Ts'] := boolp.pselect (coerce T s').
-    have ? := coerce_eq Ts'; subst T'.
+  have [Ts'|Ts'] := boolP (coercible T s').
+    have ? := coercible_eq Ts'; subst T'.
     exact: NthError H.
   exact: NthError_nocoerce H Ts'.
 exact: NthError_None.
@@ -374,7 +373,7 @@ Lemma cput_then_fail T1 T2 T1' e (s1' : coq_type T1')
     (r2 : loc T2) (s2 : coq_type T2)
     (r1 : loc T1) (s1 : coq_type T1) :
   nth_error (ofEnv e) (loc_id r1) = Some (mkbind s1') ->
-  ~ coerce T1 s1' ->
+  ~~ coercible T1 s1' ->
   (cput r2 s2 >> cput r1 s1) e = fail.
 Proof.
 move=> Hr1 T1s'.
@@ -389,7 +388,7 @@ have [v Hr2|T2' v Hr2 T2v|Hr2] := ntherrorP e r2; last first.
     subst T2.
     rewrite coerce_Some//=.
     move: Hr1; rewrite Hr Hr2 => -[?]; subst T1' => _.
-    by rewrite coerce_Some // in T1s'.
+    by rewrite coercible_Some // in T1s'.
   + rewrite (nocoerce_cput _ _ T1s')//=.
     by rewrite (@nth_error_set_nth_other _ _ _ _ _ (mkbind s1')).
 Qed.
@@ -458,7 +457,7 @@ have [u Hr1|T1' s1' Hr1 T1s'|Hr1] := ntherrorP e r1.
   + rewrite [RHS]MS_bindE (nocoerce_cget _ T2s')// bindfailf.
     rewrite !MS_bindE /cput Hr1 coerce_Some bindretf//=.
     rewrite MS_bindE /cget/= (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym//.
-    by move: (T2s'); case: coerce.
+    by rewrite not_coercible.
   + rewrite [in RHS]MS_bindE None_cget// bindfailf.
     rewrite MS_bindE /cput Hr1 coerce_Some bindretf/=.
     by rewrite MS_bindE /cget (nth_error_set_nth_none _ _ Hr2 Hr1).