Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coercible #121

Merged
merged 1 commit into from
Aug 5, 2023
Merged

coercible #121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 11 additions & 15 deletions monad_model.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 :
Expand All @@ -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.
Expand Down Expand Up @@ -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'.
Expand All @@ -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.
Expand Down Expand Up @@ -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).
Expand Down
35 changes: 27 additions & 8 deletions monae_lib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
21 changes: 10 additions & 11 deletions typed_store_model.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand All @@ -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 :
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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'.
Expand All @@ -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.
Expand Down Expand Up @@ -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).
Expand Down
Loading