Merge pull request #470 from MetaCoq/eval-fix-optimized

Optimizing the fixpoint evaluation rule

Author: mattam82

erasure/theories/EArities.v

@@ -518,14 +518,12 @@ Qed.
 
 Lemma Is_type_eval (Σ : global_env_ext) t v:
   wf Σ ->
+  axiom_free Σ ->
   eval Σ t v ->
   isErasable Σ [] t ->
   isErasable Σ [] v.
 Proof.
   intros; eapply Is_type_red. eauto.
-  eapply wcbeval_red; eauto.
   red in X1. destruct X1 as [T [HT _]].
-  eapply typecheck_closed in HT as [_ HT]; auto. 
-  apply andP in HT. now destruct HT.
-  eauto.
+  eapply wcbeval_red; eauto. assumption.
 Qed.

erasure/theories/EWcbvEval.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license.   *)
 Set Warnings "-notation-overridden".
 
-From Coq Require Import Arith Bool List Program.
+From Coq Require Import Arith Bool List Program Lia.
 From Equations Require Import Equations.
 From MetaCoq.Template Require Import config utils.
 From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst ETyping.
@@ -52,12 +52,11 @@ Definition cunfold_fix (mfix : mfixpoint term) (idx : nat) :=
   | None => None
   end.
 
-Definition isStuckFix t args :=
+Definition isStuckFix t (args : list term) :=
   match t with
   | tFix mfix idx =>
     match cunfold_fix mfix idx with
-    | Some (narg, fn) =>
-      ~~ is_nth_constructor_app_or_box narg args
+    | Some (narg, fn) => #|args| <=? narg
     | None => false
     end
   | _ => false
@@ -114,12 +113,10 @@ Section Wcbv.
       eval (tCase (ind, pars) discr brs) res
 
   (** Fix unfolding, with guard *)
-  | eval_fix f mfix idx argsv a av narg fn res :
+  | eval_fix f mfix idx argsv a av fn res :
       eval f (mkApps (tFix mfix idx) argsv) ->
       eval a av ->
-      cunfold_fix mfix idx = Some (narg, fn) ->
-      #|argsv| = narg ->
-      is_constructor_app_or_box av ->
+      cunfold_fix mfix idx = Some (#|argsv|, fn) ->
       eval (tApp (mkApps fn argsv) av) res ->
       eval (tApp f a) res
 
@@ -128,7 +125,7 @@ Section Wcbv.
       eval f (mkApps (tFix mfix idx) argsv) ->
       eval a av ->
       cunfold_fix mfix idx = Some (narg, fn) ->
-      (#|argsv| <> narg \/ (#|argsv| = narg /\ ~~is_constructor_app_or_box av)) ->
+      (#|argsv| < narg) ->
       eval (tApp f a) (tApp (mkApps (tFix mfix idx) argsv) av)
 
   (** CoFix-case unfolding *)
@@ -285,24 +282,13 @@ Section Wcbv.
         apply (value_stuck_fix _ [av]); [easy|].
         cbn.
         destruct (cunfold_fix mfix idx) as [(? & ?)|]; [|easy].
-        noconf H1.
-        destruct H2 as [|(<- & ?)]; [|easy].
-        unfold is_nth_constructor_app_or_box.
-        now rewrite (proj2 (nth_error_None _ _));
-          cbn in *.
+        noconf H1. destruct narg; auto. lia.
       + easy.
       + eapply value_stuck_fix; [now apply Forall_app_inv|].
         unfold isStuckFix in *.
         destruct (cunfold_fix mfix idx) as [(? & ?)|]; [|easy].
-        noconf H1.
-        unfold is_nth_constructor_app_or_box in *.
-        destruct H2 as [|(<- & ?)]; [|now rewrite nth_error_snoc].
-        destruct (Nat.ltb_spec #|argsv| narg).
-        * rewrite (proj2 (nth_error_None _ _)); [|easy].
-          rewrite app_length.
-          cbn.
-          easy.
-        * now rewrite nth_error_app1.
+        noconf H1. rewrite app_length; simpl.
+        eapply Nat.leb_le. lia.
 
     - destruct (mkApps_elim f' [a']).
       eapply value_mkApps_inv in IHeval1 => //.
@@ -320,15 +306,14 @@ Section Wcbv.
         rewrite orb_true_r orb_true_l in H0. easy.
   Qed.
 
-  Lemma closed_unfold_fix_cunfold_eq mfix idx : 
+  Lemma closed_fix_substl_subst_eq {mfix idx d} : 
     closed (tFix mfix idx) ->
-    unfold_fix mfix idx = cunfold_fix mfix idx.
+    nth_error mfix idx = Some d ->
+    subst0 (fix_subst mfix) (dbody d) = substl (fix_subst mfix) (dbody d).
   Proof.  
-    unfold unfold_fix, cunfold_fix.
-    destruct (nth_error mfix idx) eqn:Heq => //.
     move=> /= Hf; f_equal; f_equal.
     have clfix : All (closedn 0) (fix_subst mfix).
-    { clear Heq d idx.
+    { clear idx.
       solve_all.
       unfold fix_subst.
       move: #|mfix| => n.
@@ -340,11 +325,22 @@ Section Wcbv.
     now rewrite subst_empty.
     move=> Ha; depelim Ha.
     simpl in *.
+    intros hnth.
     rewrite -IHfix_subst => //.
     rewrite (subst_app_decomp [_]). simpl.
     f_equal. rewrite lift_closed // closed_subst //.
   Qed.
 
+  Lemma closed_unfold_fix_cunfold_eq mfix idx : 
+    closed (tFix mfix idx) ->
+    unfold_fix mfix idx = cunfold_fix mfix idx.
+  Proof.
+    unfold unfold_fix, cunfold_fix.
+    destruct (nth_error mfix idx) eqn:Heq => //.
+    intros cl; f_equal; f_equal.
+    now rewrite (closed_fix_substl_subst_eq cl).
+  Qed.
+
   Lemma closed_unfold_cofix_cunfold_eq mfix idx : 
     closed (tCoFix mfix idx) ->
     unfold_cofix mfix idx = cunfold_cofix mfix idx.
@@ -390,6 +386,106 @@ Qed.
 
 Derive NoConfusionHom for EAst.global_decl.
 
+
+Lemma Forall_Forall2_refl :
+  forall (A : Type) (R : A -> A -> Prop) (l : list A),
+  Forall (fun x : A => R x x) l -> Forall2 R l l.
+Proof.
+  induction 1; constructor; auto.
+Qed.
+
+Lemma value_head_spec_impl t :
+  implb (value_head t) (~~ (isLambda t || isFixApp t || isBox t)).
+Proof.
+  destruct t; simpl; intuition auto; eapply implybT.
+Qed.
+
+Derive Signature for Forall.
+
+Lemma eval_stuck_fix args argsv mfix idx :
+  Forall2 eval args argsv ->
+  isStuckFix (tFix mfix idx) argsv ->
+  eval (mkApps (tFix mfix idx) args) (mkApps (tFix mfix idx) argsv).
+Proof.
+  revert argsv.
+  induction args as [|a args IH] using MCList.rev_ind;
+  intros argsv all stuck.
+  - apply Forall2_length in all.
+    destruct argsv; [|easy].
+    now apply eval_atom.
+  - destruct argsv as [|? ? _] using MCList.rev_ind;
+      [apply Forall2_length in all; rewrite app_length in all; now cbn in *|].
+    apply Forall2_app_r in all as (all & ev_a).
+    rewrite <- !mkApps_nested.
+    cbn in *.
+    destruct (cunfold_fix mfix idx) as [(? & ?)|] eqn:cuf; [|easy].
+    eapply eval_fix_value.
+    + apply IH; [easy|].
+      destruct (cunfold_fix mfix idx) as [(? & ?)|]; [|easy].
+      rewrite app_length /= in stuck.
+      eapply Nat.leb_le in stuck. eapply Nat.leb_le. lia.
+    + easy.
+    + easy.
+    + rewrite app_length /= in stuck.
+      eapply Nat.leb_le in stuck; lia.
+Qed.
+
+Lemma stuck_fix_value_inv argsv mfix idx narg fn :
+  value (mkApps (tFix mfix idx) argsv) -> 
+  cunfold_fix mfix idx = Some (narg, fn) ->
+  (Forall value argsv /\ isStuckFix (tFix mfix idx) argsv).
+Proof.
+  remember (mkApps (tFix mfix idx) argsv) as tfix.
+  intros hv; revert Heqtfix.
+  induction hv using value_values_ind; intros eq; subst.
+  unfold atom in H. destruct argsv using rev_case => //.
+  split; auto. simpl. simpl in H. rewrite H0 //.
+  rewrite -mkApps_nested /= in H. depelim H.
+  solve_discr => //.
+  solve_discr.
+Qed.
+  
+Lemma stuck_fix_value_args argsv mfix idx narg fn :
+  value (mkApps (tFix mfix idx) argsv) ->
+  cunfold_fix mfix idx = Some (narg, fn) ->
+  #|argsv| <= narg.
+Proof.
+  intros val unf.
+  eapply stuck_fix_value_inv in val; eauto.
+  destruct val.
+  simpl in H0. rewrite unf in H0.
+  now eapply Nat.leb_le in H0.
+Qed.
+
+Lemma value_final e : value e -> eval e e.
+Proof.
+  induction 1 using value_values_ind; simpl; auto using value.
+  - apply Forall_Forall2_refl in H1 as H2.
+    move/implyP: (value_head_spec_impl t).
+    move/(_ H) => Ht.
+    induction l using rev_ind. simpl.
+    destruct t; try discriminate.
+    * repeat constructor.
+    * repeat constructor.
+    * rewrite -mkApps_nested.
+      eapply Forall_app in H0 as [Hl Hx]. depelim Hx.
+      eapply Forall_app in H1 as [Hl' Hx']. depelim Hx'.
+      eapply Forall2_app_inv_r in H2 as [Hl'' [Hx'' [? [? ?]]]].
+      depelim H3. depelim H4.
+      eapply eval_app_cong; auto.
+      eapply IHl; auto.
+      now eapply Forall_Forall2.
+      destruct l using rev_ind; auto.
+      eapply value_head_nApp in H.
+      rewrite isFixApp_mkApps => //.
+      rewrite -mkApps_nested; simpl.
+      rewrite orb_false_r.
+      destruct t; auto.
+  - destruct f; try discriminate.
+    apply Forall_Forall2_refl in H0.
+    now apply eval_stuck_fix.
+Qed.
+
 Unset SsrRewrite.
 Lemma eval_deterministic {t v v'} :
   eval t v ->
@@ -440,27 +536,26 @@ Proof.
     + apply IHev1 in ev'1.
       apply mkApps_eq_inj in ev'1; try easy.
       depelim ev'1.
-      noconf H2.
+      noconf H1; noconf H2.
       subst.
       apply IHev2 in ev'2; subst.
-      rewrite H4 in H.
+      noconf H0.
+      rewrite H2 in H.
       now noconf H.
     + apply IHev1 in ev'1.
       apply mkApps_eq_inj in ev'1; try easy.
       depelim ev'1.
+      noconf H1.
       noconf H2.
-      noconf H3.
       apply IHev2 in ev'2.
-      subst.
-      rewrite H4 in H.
-      noconf H.
-      destruct H5 as [|(_ & ?)]; [easy|].
-      now apply negb_true_iff in H.
+      subst. noconf H0.
+      rewrite H2 in H.
+      noconf H. lia.
     + apply IHev1 in ev'1.
       subst.
-      rewrite isFixApp_mkApps in H2 by easy.
+      rewrite isFixApp_mkApps in H0 by easy.
       cbn in *.
-      now rewrite orb_true_r in H2.
+      now rewrite orb_true_r in H0.
     + easy.
   - depelim ev'.
     + apply IHev1 in ev'1; solve_discr.
@@ -471,9 +566,7 @@ Proof.
       noconf ev'1.
       subst.
       rewrite H1 in H.
-      noconf H.
-      destruct H0 as [|(? & ?)]; [easy|].
-      now apply negb_true_iff in H0.
+      noconf H. lia.
     + apply IHev1 in ev'1.
       apply IHev2 in ev'2.
       now apply mkApps_eq_inj in ev'1 as (ev'1 & <-).