Updated to Coq 8.18.0 (small proof repair)

coq-celsius.opam

@@ -23,7 +23,7 @@ install: [
 
 depends: [
   "ocaml" {>= "4.11-flambda"}
-  "coq" {= "8.15.2"}
+  "coq" {>= "8.15.2"}
   #"coq-coq2html" {>= "1.2"}
 ]
 

src/Helpers.v

@@ -267,8 +267,8 @@ Proof.
     simpl in H1;
     fold (dom σ) in H1;
     rewrite_anywhere PeanoNat.Nat.add_1_r.
-  apply Lt.le_lt_or_eq in H1 as [H1 | H1].
-  + rewrite getObj_last2 in H; eauto using Lt.lt_S_n.
+  apply Nat.lt_eq_cases in H1 as [H1 | H1].
+  + rewrite getObj_last2 in H; eauto with lia. 
   + inversion H1; subst.
     rewrite getObj_last in H.
     invert_constructor_equalities; steps;
@@ -282,9 +282,9 @@ Lemma getVal_add:
 Proof.
   unfold getVal.
   steps.
-  assert (f < length ω \/ f = length ω) as [Hf | Hf];
+  assert (f < length ω \/ f = length ω) as [Hf | Hf] ;
     [
-      apply Lt.le_lt_or_eq, Lt.lt_n_Sm_le;
+      apply Nat.lt_eq_cases, Nat.lt_succ_r;
       pose proof (nth_error_Some (ω ++ [l]) f) as Hf;
       rewrite app_length PeanoNat.Nat.add_1_r in Hf;
       apply Hf

src/LibTactics.v

@@ -1505,7 +1505,7 @@ Ltac equates_several E cont :=
   let rec go pos :=
      match pos with
      | nil => cont tt
-     | (boxer ?n)::?pos' => equates_one n; [ instantiate; go pos' | ]
+     | (boxer ?n)::?pos' => equates_one n; [ go pos' | ]
      end in
   go all_pos.
 
@@ -1582,7 +1582,7 @@ Tactic Notation "applys_eq" constr(H) :=
     anything else *)
 
 Tactic Notation "false_goal" :=
-  elimtype False.
+  elim False.
 
 (** [false_post] is the underlying tactic used to prove goals
     of the form [False]. In the default implementation, it proves
@@ -1613,7 +1613,7 @@ Tactic Notation "tryfalse" :=
 
 Ltac false_then E cont :=
   false_goal; first
-  [ applys E; instantiate
+  [ applys E
   | forwards_then E ltac:(fun M =>
       pose M; jauto_set_hyps; intros; false) ];
   cont tt.
@@ -4864,7 +4864,7 @@ Tactic Notation "clears_last" constr(N) :=
 Axiom skip_axiom : True.
 
 Ltac skip_with_axiom :=
-  elimtype False; apply skip_axiom.
+  elim False; apply skip_axiom.
 
 Tactic Notation "skip" :=
   skip_with_axiom.

src/Reachability.v

@@ -279,19 +279,17 @@ Section Reachability_Dec.
         (exists t0 t1, tr = t0 ++ l__m :: t1 /\
                     (σ ⊨ l ⇝ l__m ↑ t0) /\
                     (σ ⊨ l__m ⇝ l' ↑ t1)).
-  Proof with (eauto using app_assoc_reverse with rch).
+  Proof with (subst; repeat rewrite -app_assoc; eauto using app_assoc with rch).
     split; intros.
     - destruct H as [H ?].
       induction H; steps.
       apply in_app_iff in H0 as [|[|]].
       + lets (t & t' & ? & ? & ?): IHreachability_trace1 H0.
-        exists t, (t'++l1::t2); subst; splits... rewrite app_assoc_reverse...
-      + subst.
-        exists t1, t2; splits...
+        exists t, (t'++l1::t2)... 
+      + exists t1, t2... 
       + lets (t & t' & ? & ? & ?): IHreachability_trace2 H0.
-        exists (t1++l1::t), t'; subst; splits... rewrite app_assoc_reverse...
-    - destruct H as (t0 & t1 & ? & ? & ?). subst.
-      split...
+        exists (t1++l1::t), t'...
+    - destruct H as (t0 & t1 & ? & ? & ?); splits... 
       apply in_elt.
   Qed.
 
@@ -300,7 +298,7 @@ Section Reachability_Dec.
       (σ ⊨ l ⇝ l' ↑ (l__m::tr)) ->
       (σ ⊨ l ⇝ l__m ↑ []) /\
         (σ ⊨ l__m ⇝ l' ↑ tr).
-  Proof with (eauto using app_assoc_reverse with rch).
+  Proof with (eauto using app_assoc with rch).
     intros.
     remember (l__m::tr) as T. gen l__m tr.
     induction H; intros; steps;

src/Soundness.v

@@ -39,7 +39,7 @@ Proof with (unfold A, B, C, Entry; simpl; eauto with typ).
     + intros. inverts H.
   - (* Class Entry *)
     assert (P_hots []) by (unfold P_hots; eauto using Forall).
-    steps; try lia...
+    steps ; try lia.
     + eapply t_new_hot...
     + eapply t_new_hot...
     + eapply t_new_hot...
@@ -67,7 +67,7 @@ Theorem weakening: forall Γ Γ' U e T,
     S_Typs Γ' Γ ->
     ((Γ, U) ⊢ e : T) ->
     ((Γ', U) ⊢ e : T).
-Proof with (meta; eauto using expr_typing with typ lia).
+Proof with (meta; eauto 4 using expr_typing with typ lia).
   intros.
   lets: S_Typs_weakening H. clear H. gen Γ'.
   induction H0 using typing_ind with
@@ -76,8 +76,9 @@ Proof with (meta; eauto using expr_typing with typ lia).
                (forall x T__x, typeLookup Γ0 x = Some T__x -> exists T__x', typeLookup Γ' x = Some T__x' /\ T__x' <: T__x) ->
                ((Γ0, T0) ⊩ el : Ul) ->
                ((Γ', T0) ⊩ el : Ul));
-    intros ...
+    intros...
   eapply H1 in H__lkp as [T__x' [ ]]...
+  eapply t_block...
 Qed.
 
 (* ------------------------------------------------------------------------ *)
@@ -204,13 +205,14 @@ Lemma soundness_mtd:
           init_soundness n C I n1 n2 ρ σ Γ Σ r) ->
     (forall e m args ρ σ ψ r Γ Σ U T,
         expr_soundness (S n) (e_mtd e m args) ρ σ ψ r Γ Σ U T).
-Proof with (meta; meta_clean; eauto 2 with typ;
+Proof with (meta; eauto 2 with typ;
             try match goal with
                 | |- ?Σ ⊨ ?l : ?T => try solve [eapply vt_sub; eauto 4 with typ]
                 end) using.
   intros n [IH__expr [IH__list IH__init]];
     unfold expr_soundness, expr_list_soundness, init_soundness; intros.
   simpl in *...
+  meta_clean.
 
   (* Induction on the typing judgment *)
   eapply t_mtd_inv in H as
@@ -230,15 +232,15 @@ Proof with (meta; meta_clean; eauto 2 with typ;
   unfold methodInfo in H__mtdinfo.
   destruct (ct C) as [Args1 Flds1 Mtds1] eqn:H__ct1.
   destruct (Mtds1 m) as [[?μ__r Ts retT ?] |] eqn:H__Mtds1; [| steps] . inverts H__mtdinfo...
-  eval_dom.
+  eval_dom. 
 
   (* Destruct evaluation of arguments *)
   lets H__env0: env_typing_monotonicity H__mn0 H0.
   eval_dom. eval_wf...
   lets (?T & ?T & ? & ? & ?): H__mn0 ψ ...
   destruct_eval H__eval1 vl σ';
     lets (Σ1 & args_val & σ1 & H__r & H__mn1 & H__stk1 & H__aty1 & H__st1 & H__wf1 & H__v1) :
-    IH__list HT__args H__env0 H__st0 H__wf0 H__eval1; try inverts H__r; try congruence ...
+    IH__list HT__args H__env0 H__st0 H__wf0 H__eval1; try inverts H__r; try congruence...
   eapply eval_implies_evalP_list in H__eval1. eval_dom; eval_wf.
 
   (* Extract typing for method body from Ξ (well-typed) *)
@@ -288,13 +290,14 @@ Lemma soundness_new:
           init_soundness n C I n1 n2 ρ σ Γ Σ r) ->
     (forall C args ρ σ ψ r Γ Σ U T,
         expr_soundness (S n) (e_new C args) ρ σ ψ r Γ Σ U T).
-Proof with (meta; meta_clean; eauto 2 with typ;
+Proof with (meta;  eauto 2 with typ;
             try match goal with
                 | |- ?Σ ⊨ ?l : ?T => try solve [eapply vt_sub; eauto with typ]
                 end) using.
   intros n [IH__expr [IH__list IH__init]];
     unfold expr_soundness, expr_list_soundness, init_soundness; intros.
-  simpl in *...
+  simpl in * ...
+  meta_clean.
 
   (* Induction on the typing judgment *)
   eapply t_new_inv in H as
@@ -405,13 +408,13 @@ Lemma soundness_asgn:
           init_soundness n C I n1 n2 ρ σ Γ Σ r) ->
     (forall e1 f e2 e' ρ σ ψ r Γ Σ U T,
         expr_soundness (S n) (e_asgn e1 f e2 e') ρ σ ψ r Γ Σ U T).
-Proof with (meta; meta_clean; eauto 2 with typ;
+Proof with (meta; eauto 2 with typ;
             try match goal with
                 | |- ?Σ ⊨ ?l : ?T => try solve [eapply vt_sub; eauto with typ]
                 end) using.
   intros n [IH__expr [IH__list IH__init]];
     unfold expr_soundness, expr_list_soundness, init_soundness; intros.
-  simpl in *...
+  simpl in * ... meta_clean.
   (* Induction on typing derivation *)
   eapply t_asgn_inv in H as
       (D & ? & ? & HT__e1 & HT__e2 & ? & HT__e3) ...
@@ -484,13 +487,14 @@ Lemma soundness_init_cons:
           init_soundness n C I n1 n2 ρ σ Γ Σ r) ->
     (forall C I n1 n2 ρ σ Γ Σ r,
         init_soundness (S n) C I n1 n2 ρ σ Γ Σ r).
-Proof with (meta; meta_clean; eauto 2 with typ;
+Proof with (meta; eauto 2 with typ;
             try match goal with
                 | |- ?Σ ⊨ ?l : ?T => try solve [eapply vt_sub; eauto with typ]
                 end) using.
   intros n [IH__expr [IH__list IH__init]];
     unfold expr_soundness, expr_list_soundness, init_soundness; intros.
   simpl in *...
+  meta_clean.
   rewrite H3 in H7.
 
   (* Retrieve current field *)
@@ -541,7 +545,7 @@ Proof with (meta; meta_clean; eauto 2 with typ;
   assert (H__field: fieldType C (dom DoneFlds) = Some (C0, μ)). {
     unfold fieldType. rewrite H3.
     rewrite nth_error_app2... subst.
-    rewrite -minus_diag_reverse...
+    rewrite Nat.sub_diag...
   }
   cross_rewrites.
 
@@ -568,7 +572,7 @@ Proof with (meta; meta_clean; eauto 2 with typ;
       updates.
       lets H__initP: H__r.
       eapply init_implies_initP in H__initP;
-        updates; try rewrite app_assoc_reverse...
+        updates; try rewrite -app_assoc...
       lets H__scpInit: scp_theorem_init H__initP.
       lets: scp_theorem_expr H__eval H1...
       exists Σ2, σ2; splits...
@@ -617,7 +621,7 @@ Proof with (meta; meta_clean; eauto 2 with typ;
       updates.
       lets H__initP: H__r.
       eapply init_implies_initP in H__initP;
-        updates; try rewrite app_assoc_reverse...
+        updates; try rewrite -app_assoc...
       lets H__scpInit: scp_theorem_init H__initP.
       lets: scp_theorem_expr H__eval H1...
       exists Σ2, σ2; splits...
@@ -641,7 +645,6 @@ Theorem soundness:
        init_soundness n C I n1 n2 ρ σ Γ Σ r).
 Proof with (
     meta;
-    meta_clean;
     eauto 4 with typ wf lia;
     try match goal with
         | |- ?Σ ⊨ ?l : ?T => try solve [eapply vt_sub; eauto with typ]
@@ -721,9 +724,10 @@ Theorem Soundness :
         Σ ≼ Σ' /\
         Σ ▷ Σ' /\
         Σ ≪ Σ'.
-Proof with (eauto with typ).
+Proof with (eauto 2 with typ).
   intros.
-  lets [(Σ'& v& σ'& ?) _]: soundness n... steps.
+  edestruct (soundness n) as [(Σ'& v& σ'& ?) _]...
+  steps.
   exists Σ', v, σ'; splits...
 Qed.
 

src/Typing.v

@@ -222,7 +222,7 @@ Lemma T_Fields_In:
 Proof with (eauto using T_Fields with typ lia).
   induction  Flds1; intros.
   - simpl in H. simpl. inverts H. rewrite <- plus_n_O...
-  - simpl in H; simpl. inverts H. rewrite <- plus_Snm_nSm ...
+  - simpl in H; simpl. inverts H. rewrite <- Nat.add_succ_comm ...
 Qed.
 
 (* ------------------------------------------------------------------------ *)

src/Wellformedness.v

@@ -193,8 +193,8 @@ Proof with (updates; cross_rewrites; eauto 4 with wf ss lia).
     lets: pM_theorem_expr H__e.
     lets: pM_assign_new H__assign.
     lets (?C & ?ω & ?): getObj_Some σ I...
-    lets (?ω & ? & ?): H7 I...
-    lets (?ω & ? & ?): H8 I...
+    edestruct (H7 I) as (?ω & ? & ?)...
+    edestruct (H8 I) as (?ω & ? & ?)...
     lets: init_field H__init...
     lets: wf_assign_new C0 H__assign...
     rewrite H__ct in IH__init.