WIP: subject reducion

coq/label_lexico.v

@@ -330,3 +330,11 @@ Proof.
     try exact I; try reflexivity; try discriminate H12; try inversion H12;
       try (apply IHs1; auto).
 Qed.
+
+Lemma lexico_lt_diff s1 s2 : lexico_lt s1 s2 -> s1 <> s2.
+Proof.
+  intros Hlt He.
+  subst s2.
+  apply lexico_irrefl in Hlt.
+  assumption.
+Qed.

coq/subject_reduction.v

 Require Import Coq.Program.Equality.
 Require Import albert aux label_lexico typer.
 Require Import List.
+Require Import Lia.
 
 Hint Constructors typing_val.
 
@@ -92,15 +93,518 @@ Proof.
       * apply H1; auto. inversion H2; auto. inversion H3; auto. inversion H4; auto.
 Qed.
 
-(** Subject reduction for function *)
-Theorem sr_f : forall f G E v v' ty ty',
+Lemma sr_f_empty : forall G f v v' ty ty',
     typing_f G f ty ty' ->
     typing_val G v ty ->
-    eval_f E f v v' ->
+    eval_f E_empty f v v' ->
     typing_val G v' ty'.
 Proof.
-  intros arg G E v v' ty ty' Hf Hval Heval.
-  induction Heval.
+  intros g f v v' ty ty' Hf Hval Heval.
+  destruct f.
+  inversion Heval; subst.
+  inversion H0.
+Qed.
+
+Lemma Join_singl_left : forall {A} l (v w : String.string * A),
+    Join (v :: nil) l (w :: nil) -> l = nil /\ v = w.
+Proof.
+  intros A l v w J.
+  inversion J.
+  - split; reflexivity.
+  - inversion H3.
+  - inversion H3.
+Qed.
+
+Lemma In_sorted_split {A} {lt : A -> A -> Prop} l a :
+  Sorted.StronglySorted lt l ->
+  In a l ->
+  exists l1 l2,
+    l = l1 ++ a :: l2 /\
+    (forall x, In x l1 -> lt x a) /\
+    (forall x, In x l2 -> lt a x).
+Proof.
+  induction l as [|b l].
+  - simpl. intuition.
+  - simpl.
+    intro Hs.
+    apply Sorted.StronglySorted_inv in Hs.
+    destruct Hs as (Hs, Hf).
+    rewrite Forall_forall in Hf.
+    intros [He|Hin].
+    + subst b.
+      exists nil.
+      exists l.
+      split; [reflexivity|].
+      split; [intuition|].
+      auto.
+    + specialize (IHl Hs Hin).
+      destruct IHl as (l1, (l2, (He, (Hlow, Hhigh)))).
+      subst l.
+      exists (b :: l1).
+      exists l2.
+      split; [reflexivity|].
+      split; intro x.
+      * intros [He | Hinx].
+        -- subst x.
+           apply Hf; assumption.
+        -- auto.
+      * auto.
+Qed.
+
+Lemma In_map_rev {A B} (f : A -> B) y l : In y (map f l) -> exists x, In x l /\ y = f x.
+Proof.
+  induction l.
+  - intro H.
+    simpl in H.
+    contradiction.
+  - simpl.
+    intros [He|Hin].
+    + exists a.
+      intuition congruence.
+    + specialize (IHl Hin).
+      destruct IHl as (x, (Hx, He)).
+      exists x.
+      intuition.
+Qed.
+
+Lemma In_sorted_case {A} L l1 l2 (v1 v2 : A) f :
+  Sorted.StronglySorted lexico_lt (map f L) ->
+  (forall l v, f (l, v) = l) ->
+  In (l1, v1) L ->
+  In (l2, v2) L ->
+  l1 <> l2 \/ (l1 = l2 /\ v1 = v2).
+Proof.
+  induction L as [|(l, v) L]; simpl.
+  - contradiction.
+  - intros Hs Hf H1 H2.
+    assert (Sorted.StronglySorted lexico_lt (map f L)) as Hs2
+        by (inversion Hs; assumption).
+    destruct H1; destruct H2.
+    + right; intuition congruence.
+    + left.
+      apply (in_map f) in H0.
+      remember (map f L) as Lfst.
+      rewrite Hf in H0.
+      rewrite Hf in Hs.
+      assert (Forall (lexico_lt l) Lfst) as HF
+          by (inversion Hs; assumption).
+      rewrite Forall_forall in HF.
+      specialize (HF l2 H0).
+      apply lexico_lt_diff in HF.
+      congruence.
+    + left.
+      apply (in_map f) in H.
+      remember (map f L) as Lfst.
+      rewrite Hf in H.
+      rewrite Hf in Hs.
+      assert (Forall (lexico_lt l) Lfst) as HF
+          by (inversion Hs; assumption).
+      rewrite Forall_forall in HF.
+      specialize (HF l1 H).
+      apply lexico_lt_diff in HF.
+      congruence.
+    + apply IHL; assumption.
+Qed.
+
+Lemma map_ext {A B} (f g : A -> B) l :
+  (forall x, f x = g x) -> map f l = map g l.
+Proof.
+  intro Hext.
+  induction l; simpl.
+  - reflexivity.
+  - rewrite Hext.
+    rewrite IHl.
+    reflexivity.
+Qed.
+
+Lemma Join_nil_right {A} (l l' : list (String.string * A)) : Join l nil l' -> l = l'.
+Proof.
+  intro H.
+  inversion H; reflexivity.
+Qed.
+
+Lemma Join_nil_left {A} (l l' : list (String.string * A)) : Join nil l l' -> l = l'.
+Proof.
+  intro H.
+  inversion H; reflexivity.
+Qed.
+
+Lemma Join_length {A} (l l' l'' : list (String.string * A)) :
+  Join l l' l'' ->
+  length l'' = length l + length l'.
+Proof.
+  intro H; induction H; simpl.
+  - apply plus_n_O.
+  - reflexivity.
+  - simpl in *.
+    f_equal.
+    assumption.
+  - simpl in *.
+    f_equal.
+    rewrite IHJoin.
+    apply plus_n_Sm.
+Qed.
+
+Lemma add_n_m_n n m : n = n + m -> m = 0.
+Proof.
+  induction n; simpl.
+  - auto.
+  - intro H.
+    injection H.
+    auto.
+Qed.
+
+Lemma typing_record_length :
+  forall (G : g) (lv : list (label * value)) (lt : list (label * ty)),
+    typing_val G (val_rval (rval_record lv)) (ty_rty (rty_record lt)) ->
+    length lv = length lt.
+Proof.
+  intros G lv lt H.
+  inversion H.
+  rewrite map_length.
+  rewrite map_length.
+  reflexivity.
+Qed.
+
+Lemma Join_cons_inv {A} (L1 L2 L3 : list (String.string * A)) lv :
+  Join L1 L2 (lv :: L3) ->
+  (exists tl, L1 = lv :: tl /\ Join tl L2 L3) \/
+  (exists tl, L2 = lv :: tl /\ Join L1 tl L3).
+Proof.
+  intro H; inversion H.
+  - subst.
+    left; exists L3.
+    repeat constructor.
+  - subst.
+    right; exists L3.
+    repeat constructor.
+  - subst.
+    left.
+    exists v1.
+    auto.
+  - subst.
+    right.
+    exists v2.
+    auto.
+Qed.
+
+Lemma Join_cons_cons_inv {A} (L1 L2 L3 : list (String.string * A)) l v1 v2 :
+  Join ((l, v1) :: L1) L2 ((l, v2) :: L3) ->
+  (v1 = v2 /\ Join L1 L2 L3).
+Proof.
+  intro H.
+  inversion H; subst; split; try reflexivity; try constructor; try assumption.
+  - apply lexico_lt_diff in H8.
+    congruence.
+  - apply lexico_lt_diff in H8.
+    congruence.
+Qed.
+
+Lemma typing_record_join G :
+  forall vs vs' vs'',
+    Join vs vs' vs'' ->
+    forall tys tys' tys'',
+        Join tys tys' tys'' ->
+        typing_val G (val_rval (rval_record vs)) (ty_rty (rty_record tys)) ->
+        typing_val G (val_rval (rval_record vs')) (ty_rty (rty_record tys')) ->
+        typing_val G (val_rval (rval_record vs'')) (ty_rty (rty_record tys'')).
+Proof.
+  intros vs vs' vs'' HJv; induction HJv; intros tys tys' tys'' HJt Hv Hv'.
+  - apply typing_record_nil_inv_l in Hv'.
+    subst tys'.
+    apply Join_nil_right in HJt.
+    subst tys''.
+    exact Hv.
+  - apply typing_record_nil_inv_l in Hv.
+    subst tys.
+    apply Join_nil_left in HJt.
+    subst tys''.
+    exact Hv'.
+  - generalize (typing_record_cons_ex_l G _ _ _ _ Hv).
+    intros (ty, (tystl, He)); subst tys; rename tystl into tys.
+    generalize (typing_record_cons_ex_l G _ _ _ _ Hv').
+    intros (ty', (tys'tl, He)); subst tys'; rename tys'tl into tys'.
+    inversion HJt.
+    + subst.
+      apply typing_record_cons_inv in Hv.
+      destruct Hv as (Ht1, Hv).
+      apply typing_record_cons_inv in Hv'.
+      destruct Hv' as (Ht2, Hv').
+      apply typing_record_cons; try assumption.
+      apply (IHHJv tys ((l2, ty') :: tys')); try assumption.
+      apply typing_record_cons; assumption.
+    + apply lexico_antirefl in H; contradiction.
+  - generalize (typing_record_cons_ex_l G _ _ _ _ Hv).
+    intros (ty, (tystl, He)); subst tys; rename tystl into tys.
+    generalize (typing_record_cons_ex_l G _ _ _ _ Hv').
+    intros (ty', (tys'tl, He)); subst tys'; rename tys'tl into tys'.
+    inversion HJt.
+    + apply lexico_antirefl in H; contradiction.
+    + subst.
+      apply typing_record_cons_inv in Hv.
+      destruct Hv as (Ht1, Hv).
+      apply typing_record_cons_inv in Hv'.
+      destruct Hv' as (Ht2, Hv').
+      apply typing_record_cons; try assumption.
+      apply (IHHJv ((l1, ty) :: tys) tys'); try assumption.
+      apply typing_record_cons; assumption.
+Qed.
+
+Lemma typing_record_in G : forall vs tys,
+  (forall l v ty, In (l, v) vs -> In (l, ty) tys -> typing_val G v ty) ->
+  map (fun '(l, _) => l) vs = map (fun '(l, _) => l) tys ->
+  typing_val G (val_rval (rval_record vs)) (ty_rty (rty_record tys)).
+Proof.
+  induction vs as [|(l, v) vs].
+  - intros tys Hin Hmap.
+    destruct tys; [|simpl in Hmap; discriminate].
+    apply typing_record_nil.
+  - intros tys Hin Hmap.
+    destruct tys as [|(l', ty) tys]; [simpl in Hmap; discriminate|].
+    simpl in Hmap.
+    injection Hmap; clear Hmap; intros Hl Hmap.
+    subst l'.
+    apply typing_record_cons.
+    + apply (Hin l); left; reflexivity.
+    + apply IHvs.
+      * intros l' v' ty' Hv Hty.
+        apply (Hin l'); right; assumption.
+      * assumption.
+Qed.
+
+Lemma typing_record_in_inv G : forall vs tys,
+    typing_val G (val_rval (rval_record vs)) (ty_rty (rty_record tys)) ->
+    Sorted.StronglySorted lexico_lt (map (fun '(l, _) => l) tys) ->
+    (forall l v ty, In (l, v) vs -> In (l, ty) tys -> typing_val G v ty) /\
+    map (fun '(l, _) => l) vs = map (fun '(l, _) => l) tys.
+Proof.
+  induction vs as [|(l, v) vs]; intros tys Hval Hwf; split.
+  - intros l v ty Hin.
+    inversion Hin.
+  - apply typing_record_nil_inv_l in Hval.
+    subst tys.
+    reflexivity.
+  - intros l' v' ty' [He|Htl].
+    + injection He; clear He; intros; subst.
+      generalize (typing_record_cons_ex_l _ _ _ _ _ Hval).
+      intros (ty'', (lts, He)).
+      subst tys; rename lts into tys.
+      apply (Sorted_not_In l' ty' ty') in Hwf.
+      destruct H1; [|contradiction].
+      injection H; intros; subst.
+      apply typing_record_cons_inv in Hval; destruct Hval; assumption.
+    + intro Hin_ty.
+      generalize (typing_record_cons_ex_l _ _ _ _ _ Hval).
+      intros (ty'', (lts, He)).
+      subst tys; rename lts into tys.
+      specialize (IHvs tys).
+      apply typing_record_cons_inv in Hval.
+      destruct Hval as (Hv, Hval).
+      specialize (IHvs Hval).
+      simpl in Hwf; inversion Hwf.
+      specialize (IHvs H1).
+      destruct IHvs as (IH, Hmap).
+      apply (IH l').
+      * assumption.
+      * destruct Hin_ty.
+        -- subst.
+           exfalso.
+           apply (in_map (fun '(l, _) => l)) in Htl.
+           rewrite Hmap in Htl.
+           rewrite Forall_forall in H2.
+           specialize (H2 l' Htl).
+           injection H3; intros; subst.
+           apply lexico_lt_diff in H2.
+           auto.
+        -- subst.
+           assumption.
+  - generalize (typing_record_cons_ex_l _ _ _ _ _ Hval).
+    intros (ty'', (lts, He)).
+    subst tys; rename lts into tys.
+    specialize (IHvs tys).
+    apply typing_record_cons_inv in Hval.
+    destruct Hval as (Hv, Hval).
+    specialize (IHvs Hval).
+    simpl in Hwf; inversion Hwf.
+    specialize (IHvs H1).
+    destruct IHvs as (IH, Hmap).
+    subst.
+    simpl.
+    f_equal.
+    assumption.
+Qed.
+
+(* Subject reduction for rhs depends on subject reduction for functions *)
+Lemma sr_f_rhs : forall G E,
+    (forall f v v' ty ty',
+        typing_f G f ty ty' ->
+        typing_val G v ty ->
+        eval_f E f v v' ->
+        typing_val G v' ty') ->
+    (forall r v v' ty ty',
+        typing_rhs G r ty ty' ->
+        typing_val G v ty ->
+        eval_rhs E r v v' ->
+        typing_val G v' ty').
+Proof.
+  intros G E sr_f  r v v' ty ty' Hr Hval Heval.
+  destruct r; inversion Hr; inversion Heval; subst.
+  - (* arg *)
+    eapply sr_arg; eassumption.
+  - (* app *)
+    assert (typing_val G val' ty'0).
+    + eapply sr_arg; eassumption.
+    + eapply sr_f; eassumption.
+  - (* record projection r.l --> v : ty when r : tys --> vs, vs.l = v : ty
+        r = l @ r'; vs = l @ vs'
+ *)
+    rename var into r.
+    rename v' into v.
+    rename ty' into ty.
+    rename rval' into vs.
+    rename rty' into tys.
+    rename rty5 into r'.
+    rename rval5 into vs'.
+    clear E sr_f Hr Heval.
+    rename H2 into H_Join_ty.
+    rename H11 into H_Join_val.
+    rename H5 into HWF.
+    destruct r' as [r'].
+    destruct tys as [tys].
+    destruct vs' as [vs'].
+    destruct vs as [vs].
+    apply typing_record_cons_inv in Hval.
+    destruct Hval as (Hvs, _).
+    apply Join_In_l_cons in H_Join_val; clear vs'.
+    apply Join_In_l_cons in H_Join_ty; clear r'.
+    inversion HWF; subst.
+    clear HWF H1 H3.
+    rename H0 into Hsorted.
+    inversion Hvs; subst.
+    rename H2 into Hin_ty.
+    apply Hin_ty; clear Hin_ty.
+    induction l__val__ty__list as [|((l', v'), ty') L]; simpl in *.
+    * contradiction.
+    * destruct H_Join_ty as [He|Hin_ty].
+       -- injection He; intros; subst; clear He.
+          destruct H_Join_val as [He|Hin_val].
+          ++ left; congruence.
+          ++ exfalso.
+             apply (lexico_lt_diff l l); [|reflexivity].
+             assert (Forall (lexico_lt l)
+                            (map (fun pat_ : label * albert.ty => let (l__, _) := pat_ in l__)
+                                 (map
+                                    (fun pat_ : label * value * albert.ty =>
+                                       let (p, ty__) := pat_ in let (l__, _) := p in (l__, ty__))
+                                    L))) as Hlt
+                 by (inversion Hsorted; assumption).
+             rewrite Forall_forall in Hlt.
+             apply Hlt; clear Hlt.
+             rewrite map_map.
+             apply (in_map (fun '(l, _) => l)) in Hin_val.
+             simpl in Hin_val.
+             rewrite map_map in Hin_val.
+             erewrite map_ext;
+               [apply Hin_val|intros ((l'', v''), ty'); reflexivity].
+       -- destruct H_Join_val as [He|Hin_val].
+          ++ exfalso.
+             injection He; intros; subst; clear He.
+             apply (lexico_lt_diff l l); [|reflexivity].
+             assert (Forall (lexico_lt l)
+                            (map (fun pat_ : label * albert.ty => let (l__, _) := pat_ in l__)
+                                 (map
+                                    (fun pat_ : label * value * albert.ty =>
+                                       let (p, ty__) := pat_ in let (l__, _) := p in (l__, ty__))
+                                    L))) as Hlt
+                 by (inversion Hsorted; assumption).
+             rewrite Forall_forall in Hlt.
+             apply Hlt; clear Hlt.
+             rewrite map_map.
+             apply (in_map (fun '(l, _) => l)) in Hin_ty.
+             simpl in Hin_ty.
+             rewrite map_map in Hin_ty.
+             erewrite map_ext;
+               [apply Hin_ty|intros ((l', v'), ty''); reflexivity].
+          ++ right.
+             apply typing_record_cons_inv in Hvs;
+               destruct Hvs as (Hval, Hrval).
+             inversion Hsorted.
+             apply IHL; assumption.
+
+  - (* record update { r with ls = xs }
+          r : { ls : bs } @ ({ labs : as } = a) @  = tys
+          r --> { ls = vbs } @ ({ labs = vas } = lvas)  = vs
+          xs --> vbs'
+          { r with ls = xs } : tys --> ({ls = vbs'} @ { labs = vas }) = vs'
+     *)
+    rename var into r.
+    rename rty' into tys.
+    destruct rval' as [vs].
+    destruct rval'' as [vs'].
+    destruct rty5 as [a].
+    destruct tys as [tys].
+    destruct rval5 as [lvas].
+    simpl in *.
+    apply typing_record_cons_inv in Hval.
+    destruct Hval as (Hvs, Hval).
+    do 2 rewrite app_nil_r in *.
+    clear Heval Hr r E sr_f.
+    refine (typing_record_join G _ _ _ H12 _ _ _ H5 _ _).
+    + apply typing_record_in.
+      * intros l v ty.
+        intros Hinv Hinty.
+        apply In_map_rev in Hinv; simpl in Hinv.
+        destruct Hinv as ((((l', var), val), val'), (Hinv, He)).
+        injection He; clear He; intros; subst.
+        apply In_map_rev in Hinty; simpl in Hinty.
+        destruct Hinty as (((l'', var'), ty'), (Hinty, He)).
+        injection He; clear He; intros; subst.
+        assert (var = var').
+        -- apply (in_map (fun pat_ : label * label * value * value =>
+          let (p, _) := pat_ in
+          let (p0, _) := p in let (l__, var__) := p0 in (l__, var__))) in Hinv.
+           rewrite H7 in Hinv.
+           apply (in_map (fun pat_ : label * label * ty =>
+                            let (p, _) := pat_ in let (l__, var__) := p in (l__, var__))) in Hinty.
+           remember (map
+              (fun pat_ : label * label * ty =>
+               let (p, _) := pat_ in let (l__, var__) := p in (l__, var__))
+              l__var__ty__list) as L.
+           generalize (In_sorted_case L l'' l'' var var' (fun '(l, _) => l)).
+           intro Hcase.
+           refine (match (Hcase _ _ _ _) with or_introl HN => False_rect _ (HN eq_refl) | or_intror (conj _ H) => H end).
+           ++ subst L.
+              rewrite map_map.
+              inversion H2.
+Admitted.
+
+(** Subject reduction for function, right-hand sides, and instructions *)
+Theorem sr_f_rhs_i : forall G E,
+    (forall f v v' ty ty',
+        typing_f G f ty ty' ->
+        typing_val G v ty ->
+        eval_f E f v v' ->
+        typing_val G v' ty') /\
+    (forall r v v' ty ty',
+        typing_rhs G r ty ty' ->
+        typing_val G v ty ->
+        eval_rhs E r v v' ->
+        typing_val G v' ty') /\
+    (forall i v v' ty ty',
+        typing_instr G i ty ty' ->
+        typing_val G v ty ->
+        eval_instr E i v v' ->
+        typing_val G v' ty').
+Proof.
+  intro G; induction E.
+  - split; [|split].
+    + apply sr_f_empty.
+    + apply sr_f_rhs.
+      apply sr_f_empty.
+    + admit.
+  - split; [|split].
+    
+        
 Admitted.
 
 Lemma wf_record_cons_inv : forall G lt l ty,

ott/base.ott

@@ -251,7 +251,7 @@ by
     { l : ty } @ rty = rty'
     g |- rty'
     ------------------------------------- :: projection
-    g |- var . l : rty' => ty
+    g |- var . l : { var : rty' } => ty
 
     g |- rty'
     { l_1 : ty_1 ; .. ; l_n : ty_n } @ rty = rty'
@@ -312,7 +312,7 @@ defns
 
     { l = val } @ rval = rval'
     ----------------------------------------- :: projection
-    E |- var.l / rval' -> val
+    E |- var.l / { var = rval' } -> val
 
     { l_1 = val'_1 ; .. ; l_n = val'_n } @ rval = rval'
     { l_1 = val_1 ; .. ; l_n = val_n } @ rval = rval''

ott/toplevel_definition.ott

@@ -25,7 +25,8 @@ g :: 'g_' ::= {{tex \Gamma}} {{com Typing context (for inlined definitions)}}
   | g , tvar = ty :: :: typedef
 
 E :: 'E_' ::= {{com Semantic context (for function definitions)}}
-  | E, fvar = instruction :: :: fdef
+  | . :: :: empty
+  | E , fvar = instruction :: :: fdef
 
 formula :: 'formula_' ::=
   | tvar != tvar' :: :: tvardiff {{coq [[tvar]] <> [[tvar']]}}