Merge pull request #593 from mattam82/fix-simplify-opacity-and-funelim

Fix `simplify` breaking the transparency/opaque status of constants a…

.gitignore

@@ -63,3 +63,4 @@ doc/equations_intro.tex
 doc/equations_intro.html
 doc/coqdoc.css
 doc/index.html
+.vscode/Coq-Equations.code-workspace

_CoqProject

@@ -50,6 +50,7 @@ theories/Init.v
 theories/Signature.v
 theories/CoreTactics.v
 
+theories/Prop/SigmaNotations.v
 theories/Prop/Logic.v
 theories/Prop/Classes.v
 theories/Prop/EqDec.v

examples/AlmostFull.v

@@ -749,7 +749,7 @@ Section SCT.
     now exists fz.
     specialize (H x y x y). rewrite -> H in Hfs.
     destruct Hfs. now exists (fs x0).
-    intros [k Hk]. depelim k. intuition. right.
+    intros [k Hk]. depelim k. now left. right.
     rewrite (H x y). now exists k.
   Qed.
 
@@ -1053,7 +1053,7 @@ Section SCT.
     | None => forall a, In a l -> f a = None
     end.
   Proof.
-    funelim (find_opt l f); intros. elim H.
+    funelim (find_opt l f); cbn; intros. elim H.
     exists x; simpl; intuition eauto.
     destruct (find_opt xs f); now firstorder subst.
   Qed.

examples/MoreDep.v

@@ -160,7 +160,7 @@ End depth.
 
 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
 Proof.
-  intros. funelim (depth Nat.min t);
+  intros. funelim (depth Nat.min t); cbn;
             auto;
   match goal with
   | [ |- context[min ?X ?Y] ] =>
@@ -173,7 +173,7 @@ Lemma depth_max' : forall c n (t : rbtree c n), match c with
                                                   | Black => depth max t <= 2 * n
                                                 end.
 Proof.
-  intros; funelim (depth Nat.max t); auto;
+  intros; funelim (depth Nat.max t); cbn; auto;
   match goal with
   | [ |- context[max ?X ?Y] ] =>
       let H := fresh in destruct (Nat.max_dec X Y) as [H|H]; rewrite H
@@ -298,7 +298,7 @@ Section insert.
     Qed.
 
     Ltac present_insert t t0 :=
-      intros; funelim (insert t); generalize (present_ins t0);
+      intros; funelim (insert t); cbn; generalize (present_ins t0);
       try rewrite present_insResult_equation_1; try rewrite present_insResult_equation_2;
       funelim (ins t0); intro; assumption.
 

examples/RoseTree.v

@@ -70,7 +70,8 @@ Module RoseTree.
     Lemma elements_equation (r : t) : elements r = elements_def r.
     Proof.
       funelim (elements r); simp elements_def; trivial. f_equal.
-      induction l; simpl; auto. simp map_In. rewrite H. rewrite IHl; auto.
+      rewrite map_In_spec. clear Heqcall.
+      induction l; simpl; auto. rewrite H. rewrite IHl; auto.
       intros. apply H. now constructor 2. now constructor.
     Qed.
 

examples/STLC.v

@@ -694,7 +694,7 @@ Lemma hereditary_subst_type Γ Γ' t T u U : Γ |-- u : U -> Γ' @ (U :: Γ) |--
     (Γ' @ Γ |-- t' : T /\ (forall ty prf, o = Some (exist ty prf) -> ty = T)).
 Proof.
   intros.
-  funelim (hereditary_subst (U, u, t) (length Γ'));
+  funelim (hereditary_subst (U, u, t) (length Γ')) Heqcall; cbn in Heqcall |- *;
     DepElim.simpl_dep_elim; subst;
     try (split; [ (intros; try discriminate) | solve [ intros; discriminate ] ]);
     DepElim.simplify_dep_elim.
@@ -733,12 +733,13 @@ Proof.
     on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ).
     dependent elimination H2 as [application _ U T f arg tyfn tyu].
     specialize (H _ _ H1 tyu).
-    specialize (Hind _ _ H1 tyfn). rewrite Heq in Hind.
+    specialize (Hind _ _ H1 tyfn). cbn in Heqcall. rewrite Heq0 in Hind.
     destruct Hind as [Ht' Ht''].
     dependent elimination Ht' as [abstraction _ U T abs tyabs].
     eqns_specialize_eqs Ht''. noconf Ht''.
     destruct H as [Ht tty].
-    specialize (H0 _ [] _ _ _ _ Ht tyabs eq_refl).
+    specialize (H0 _ [] _ _ _ _ Ht tyabs eq_refl Heqhsubst0). cbn in H0.
+    rewrite <- Heqhsubst0 in H0.
     destruct H0 as [H0 H5].
     split; auto.
     intros ty prf0 Heq'.
@@ -756,7 +757,8 @@ Proof.
   (* Fst redex *)
   - simpl in *.
     depelim H0. specialize (Hind _ _ H H0).
-    rewrite Heq in Hind.
+    cbn in Heqcall.
+    rewrite Heq0 in Hind.
     destruct Hind. depelim H1. intuition auto.
     eqns_specialize_eqs H2. noconf H2.
     now noconf H1.
@@ -770,7 +772,7 @@ Proof.
 
   (* Snd redex *)
   - simpl. depelim H0. specialize (Hind _ _ H H0).
-    rewrite Heq in Hind.
+    rewrite Heq0 in Hind.
     destruct Hind. depelim H1. intuition auto.
     eqns_specialize_eqs H2. noconf H2.
     now noconf H1.
@@ -812,13 +814,15 @@ Proof.
   simpl. simpl in *.
 
   (** Lambda *)
-  - on_call hereditary_subst
+  - cbn in *.
+    on_call hereditary_subst
             ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *).
     split; intros Hsyn; [| elim (synth_arrow False Hsyn)].
 
     invert_term. constructor. 
     specialize (Hind _ _ _ (A0 :: Γ') eq_refl). simpl in *.
-    specialize (Hind _ B Hu).
+    specialize (Hind Heqhsubst _ B Hu).
+    rewrite <- Heqhsubst in Hind.
     destruct o as [[ty prf]|], Hind as [Hind0 Hind1].
     apply Hind0; eauto. eauto.
     elim (synth_arrow False H0).
@@ -869,7 +873,7 @@ Proof.
   - cbn. on_call (hereditary_subst (A,a,arg))
             ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *).
     specialize (H0 _ _ _ [] eq_refl).
-    rewrite Heq in Hind.
+    rewrite Heq0 in Hind.
     revert H0.
     on_call hereditary_subst
             ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *).
@@ -885,11 +889,13 @@ Proof.
 
     destruct o; try destruct h; destruct H.
     destruct (H H2). subst x.
-    specialize (H0 _ B' H7).
+    specialize (H0 Heqhsubst0 _ B' H7).
+    rewrite <- Heqhsubst0 in H0.
     destruct o0 as [[ty typrf]|]; destruct H0 as [Hcheck Hinf].
     now apply Hcheck. now apply Hcheck.
 
-    specialize (H0 _ B' (H H2)).
+    specialize (H0 Heqhsubst0 _ B' (H H2)).
+    rewrite <- Heqhsubst0 in H0.
     destruct o0 as [[ty typrf]|]; destruct H0 as [Hcheck Hinf].
     now apply Hcheck. now apply Hcheck.
 
@@ -937,12 +943,12 @@ Proof.
       constructor; auto.
 
   (* Pair *)
-  - simpl in Heq. autorewrite with is_pair in Heq. simpl in prf.
+  - simpl in Heq0. autorewrite with is_pair in Heq. simpl in prf.
     intros Γ T Hu.
     assert( (Γ' @ (A :: Γ) |-- Fst t' => T → Γ' @ Γ |-- u <= T ∧ a' = T)).
     intros Ht; depelim Ht. specialize (Hind _ (T × B) Hu). revert Hind.
     on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *).
-    noconf Heq.
+    noconf Heq0. cbn in Heqcall. 
     intros [Hind Hind'].
     specialize (Hind' Ht). destruct Hind' as [H0 H1]. noconf H1.
     depelim H0. split; auto.
@@ -971,7 +977,7 @@ Proof.
     intros Ht; depelim Ht. specialize (Hind _ (A0 × T) Hu). revert Hind.
     on_call hereditary_subst
             ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *).
-    noconf Heq.
+    noconf Heq0.
     intros [Hind Hind'].
     specialize (Hind' Ht). destruct Hind' as [H0 H1]. noconf H1.
     depelim H0. split; auto. depelim H0.

examples/definterp.v

@@ -85,6 +85,8 @@ Inductive Expr : Ctx -> Ty -> Set :=
 | var {Γ} {t} : In t Γ -> Expr Γ t
 | abs {Γ} {t u} : Expr (t :: Γ) u -> Expr Γ (t ⇒ u)
 | app {Γ} {t u} : Expr Γ (t ⇒ u) -> Expr Γ t -> Expr Γ u
+
+
 | new {Γ t} : Expr Γ t -> Expr Γ (ref t)
 | deref {Γ t} : Expr Γ (ref t) -> Expr Γ t
 | assign {Γ t} : Expr Γ (ref t) -> Expr Γ t -> Expr Γ unit.

examples/quicksort.v

@@ -4,6 +4,8 @@ Require Import Vector.
 Notation vector := t.
 Derive NoConfusion NoConfusionHom for vector.
 
+Set Equations Transparent.
+
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
 
@@ -32,7 +34,7 @@ Lemma All_app {A P n m} (v : vector A n) (w : vector A m) :
   @All A P _ v -> All P w -> All P (app v w).
 Proof.
   funelim (app v w). auto.
-  intros. depelim H0; simpl in *. constructor; auto.
+  intros. depelim H0; simp app in *. econstructor; auto.
 Qed.
 
 Lemma In_All {A P n} (v : vector A n) : All P v <-> (forall x, In x v -> P x).
@@ -65,8 +67,8 @@ Admitted.
 Lemma In_app {A n m} (v : vector A n) (w : vector A m) (a : A) : In a v \/ In a w <-> In a (app v w).
 Proof.
   funelim (app v w). intuition. depelim H0.
-  split. intros; depelim H0; simp In in *; intuition. simp In in *. intuition.
-  apply H in H1. intuition.
+  split; intros; depelim H0; cbn; simp In app in *; intuition eauto with *; simp In in *.
+  apply H in H0. intuition.
 Qed.
 Require Import Sumbool.
 
@@ -125,7 +127,9 @@ Section QuickSort.
     simpl. destruct (eq_sym (plus_n_Sm k l)). simpl.
     intuition.
     apply Sorted_app; auto. constructor.
-    apply In_All. intros x1 Inx1. apply H2 in Inx1. eapply leb_inverse.
+    apply In_All. intros x1 Inx1. apply H2 in Inx1.
+    specialize (i x1).
+    eapply leb_inverse.
 
     eapply All_In_All; eauto. eapply All_impl; eauto. simpl. intros x1 [inx1 lebx1].
     apply leb_inverse; assumption. intuition.

src/depelim.ml

@@ -283,7 +283,7 @@ let whd_head env sigma t =
     mkApp (eq, Array.map (Tacred.whd_simpl env sigma) args)
   | _ -> t
 
-let specialize_eqs ~with_block id =
+let specialize_eqs ?with_block id =
   Proofview.Goal.enter begin fun gl ->
   let open Tacticals in
   let open Tacmach in
@@ -295,19 +295,19 @@ let specialize_eqs ~with_block id =
     | exception Evarconv.UnableToUnify _ -> false
     | evm -> evars := evm; true
   in
-  let rec aux in_block in_eqs ctx subst acc ty =
+  let rec aux block_count in_block in_eqs ctx subst acc ty =
     match kind !evars ty with
     | LetIn (na, b, t, ty) ->
       if is_global env !evars (Lazy.force coq_block) b then
-        if not with_block then aux true in_eqs ctx subst acc (subst1 mkProp ty)
-        else if in_block then acc, in_eqs, ctx, subst, (subst1 mkProp ty)
-        else aux true in_eqs ctx subst acc (subst1 mkProp ty)
+        if with_block = None then aux block_count in_block in_eqs ctx subst acc (subst1 mkProp ty)
+        else if (in_block || in_eqs) && Int.equal block_count 0 then acc, in_eqs, ctx, subst, (subst1 mkProp ty)
+        else aux (block_count - 1) true in_eqs ctx subst acc (subst1 mkProp ty)
       else if not in_block then
-        aux in_block in_eqs (make_def na (Some b) t :: ctx) subst acc ty
+        aux block_count in_block in_eqs (make_def na (Some b) t :: ctx) subst acc ty
       else
-        aux in_block in_eqs ctx (make_def na (Some b) t :: subst) acc ty
+        aux block_count in_block in_eqs ctx (make_def na (Some b) t :: subst) acc ty
     | Prod (na, t, b) when not in_block ->
-      aux false in_eqs (make_def na None t :: ctx) subst (mkApp (lift 1 acc, [| mkRel 1 |])) b
+      aux block_count false in_eqs (make_def na None t :: ctx) subst (mkApp (lift 1 acc, [| mkRel 1 |])) b
     | Prod (na, t, b) ->
       let env' = push_rel_context ctx env in
       let env' = push_rel_context subst env' in
@@ -328,7 +328,7 @@ let specialize_eqs ~with_block id =
          let p = mkApp (eqr, [| eqty; c |]) in
          if (compare_upto_variables !evars c o) &&
             unif (push_rel_context ctx env) subst evars o c then
-           aux in_block true ctx subst (mkApp (acc, [| p |])) (subst1 p b)
+           aux block_count in_block true ctx subst (mkApp (acc, [| p |])) (subst1 p b)
          else acc, in_eqs, ctx, subst, ty
        | _ ->
          if in_eqs then
@@ -337,10 +337,11 @@ let specialize_eqs ~with_block id =
          else
            let e = evd_comb1 (Evarutil.new_evar (push_rel_context ctx env))
                evars (it_mkLambda_or_subst env t subst) in
-           aux in_block false ctx (make_def na (Some e) t :: subst) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+           aux block_count in_block false ctx (make_def na (Some e) t :: subst) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, subst, ty
   in
-  let acc, worked, ctx, subst, ty = aux (if with_block then false else true) false [] [] (mkVar id) ty in
+  let acc, worked, ctx, subst, ty = aux (match with_block with None -> 0 | Some n -> n) 
+    (match with_block with None -> true | Some _ -> false) false [] [] (mkVar id) ty in
   let subst' = nf_rel_context_evar !evars subst in
   let subst'' = List.map (fun decl ->
     let (n,b,t) = to_tuple decl in
@@ -366,11 +367,11 @@ exception Specialize
 
 open Proofview.Notations
 
-let specialize_eqs ~with_block id =
+let specialize_eqs ?with_block id =
   let open Tacticals in
   Proofview.Goal.enter begin fun gl ->
   Proofview.tclORELSE (clear [id] <*> Proofview.tclZERO Specialize) begin function
-  | (Specialize, _) -> specialize_eqs ~with_block id
+  | (Specialize, _) -> specialize_eqs ?with_block id
   | e -> tclFAIL (str "Specialization not allowed on dependent hypotheses")
   end
   end

src/depelim.mli

@@ -41,7 +41,7 @@ val derive_dep_elimination
 val pattern_call :
   ?pattern_term:bool -> constr -> unit Proofview.tactic
 
-val specialize_eqs : with_block:bool -> Names.Id.t -> unit Proofview.tactic
+val specialize_eqs : ?with_block:int -> Names.Id.t -> unit Proofview.tactic
 
 val compare_upto_variables : Evd.evar_map -> constr -> constr -> bool
 

src/g_equations.mlg

@@ -517,10 +517,10 @@ END
 
 TACTIC EXTEND eqns_specialize_eqs
 | [ "eqns_specialize_eqs" ident(i) ] -> {
-    Depelim.specialize_eqs ~with_block:false i
+    Depelim.specialize_eqs i
   }
-| [ "eqns_specialize_eqs_block" ident(i) ] -> {
-    Depelim.specialize_eqs ~with_block:true i
+| [ "eqns_specialize_eqs_block" ident(i) int_opt(n) ] -> {
+    Depelim.specialize_eqs ~with_block:(match n with None -> 1 | Some n -> n) i
   }
 END