Try progress on deterministic evaluation proofs

coq/ExpressionSemantics_det.v

@@ -46,11 +46,55 @@ Proof.
     reflexivity.
 Qed.
 
-Print Assumptions bindDelta_map_none_injective.
-
 Definition contained_delta_map dmap1 dmap2 :=
   forall (e: expr R) (v: R), dmap1 e = Some v -> dmap2 e = Some v.
 
+Instance contained_delta_map_preorder: PreOrder contained_delta_map.
+Proof.
+  constructor.
+  - unfold Reflexive, contained_delta_map; auto.
+  - unfold Transitive, contained_delta_map; auto.
+Qed.
+
+Lemma contained_delta_map_refl dmap:
+  contained_delta_map dmap dmap.
+Proof.
+  reflexivity.
+Qed.
+
+Hint Resolve contained_delta_map_refl.
+
+Lemma contained_delta_map_trans dmap1 dmap2 dmap3:
+  contained_delta_map dmap1 dmap2 -> contained_delta_map dmap2 dmap3 -> contained_delta_map dmap1 dmap3.
+Proof.
+  etransitivity; eauto.
+Qed.
+
+Lemma expr_compare_eq_equal e1 e2:
+  R_orderedExps.exprCompare e1 e2 = Eq <-> e1 = e2.
+Proof.
+  induction e1; cbn; split; intros H.
+  - destruct e2; try congruence.
+    apply nat_compare_eq in H.
+    now rewrite H.
+  - destruct e2; try congruence.
+    inversion H.
+    apply Nat.compare_refl.
+  - destruct e2; try congruence.
+Admitted.
+
+Lemma contained_delta_map_extension dmap k v:
+  contained_delta_map dmap (bindDelta dmap k v).
+Proof.
+  unfold bindDelta.
+  unfold contained_delta_map.
+  intros.
+  destruct (dmap k) eqn: Hdmapk; auto.
+  destruct R_orderedExps.eq_dec as [Heq|Heq]; auto.
+Admitted.
+
+Hint Resolve contained_delta_map_trans.
+
 Inductive eval_expr_det (E: env)
           (Gamma: expr R -> option mType)
           (DeltaMap: expr R -> option R)
@@ -446,6 +490,16 @@ Proof.
           rewrite <- Gamma_eq; auto.
 Qed.
 
+Lemma eval_expr_det_delta_map_contained E Gamma DeltaMap DeltaMap' e v m:
+  eval_expr_det E Gamma DeltaMap e v m DeltaMap' ->
+  contained_delta_map DeltaMap DeltaMap'.
+Proof.
+  revert v m DeltaMap DeltaMap'.
+  induction e; intros v__FP m__FP DeltaMap DeltaMap' Heval.
+  - inversion Heval; auto.
+  - inversion Heval; subst.
+Admitted.
+
 Lemma eval_expr_det_delta_map_dom E Gamma DeltaMap DeltaMap' DeltaMap'' e v1 v2 m1 m2:
   eval_expr_det E Gamma DeltaMap e v1 m1 DeltaMap' ->
   eval_expr_det E Gamma DeltaMap e v2 m2 DeltaMap'' ->
@@ -480,12 +534,14 @@ Proof.
         rewrite He'.
         destruct R_orderedExps.eq_dec; try apply IHe'.
         split; eauto.
-  -
+  - inversion Heval1; inversion Heval2; subst; auto.
+    specialize (IHe1 _ _ _ _ _ _ _ H6 H19).
+    (* specialize (IHe2 _ _ _ _ _ _ H10 H23). *)
 Admitted.
 
 Lemma eval_expr_det_functional E Gamma DeltaMap DeltaMap' e v1 v2 m:
   eval_expr_det E Gamma DeltaMap e v1 m DeltaMap' ->
-  eval_expr_det E Gamma DeltaMap e v2 m DeltaMap' ->
+  eval_expr_det E Gamma DeltaMap' e v2 m DeltaMap' ->
   v1 = v2.
 Proof.
   revert v1 v2 m DeltaMap DeltaMap'.
@@ -493,10 +549,11 @@ Proof.
   - inversion Heval1; inversion Heval2; subst; auto.
     now replace v1 with v2 by congruence.
   - inversion Heval1; inversion Heval2; subst; auto.
-    destruct (DeltaMap (Const m__FP v)) eqn: Hdmap.
-    + erewrite H1; eauto.
-      erewrite H8; eauto.
-    + apply bindDelta_map_none_injective in H11; subst; auto.
+    (* destruct (DeltaMap (Const m__FP v)) eqn: Hdmap. *)
+    (* + erewrite H1; eauto. *)
+    (*   erewrite H8; eauto. *)
+    (* + apply bindDelta_map_none_injective in H11; subst; auto. *)
+    admit.
   - destruct u; inversion Heval1; inversion Heval2; subst; auto.
     + cbn in *; f_equal; eapply IHe; eauto.
       admit.