Permalink
Browse files

Using hnf instead of "intro H" for forcing reduction to a product.

Added full betaiota in hnf. This seems more natural, even if it
changes the strict meaning of hnf. This is source of incompatibilities
as "intro" might succeed more often.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent f687552 commit d223f85d0fd57ce74dcdcc8690a36f1ef87b408d herbelin committed Mar 21, 2013
Showing with 32 additions and 21 deletions.
  1. +4 −0 CHANGES
  2. +4 −3 doc/refman/RefMan-tac.tex
  3. +4 −3 pretyping/tacred.ml
  4. +3 −3 tactics/tactics.ml
  5. +17 −0 test-suite/success/intros.v
  6. +0 −12 theories/Classes/Morphisms_Prop.v
View
@@ -32,6 +32,10 @@ Tactics
- Tactic notations can now be defined locally to a module (use "Local" prefix).
- Tactic "red" now reduces head beta-iota redexes (potential source of
rare incompatibilities).
+- Tactic "hnf" now reduces inner beta-iota redexes
+ (potential source of rare incompatibilities).
+- Tactic "intro H" now reduces beta-iota redexes if these hide a product
+ (potential source of rare incompatibilities).
Program
@@ -671,8 +671,8 @@ \subsection{\tt intro}
In both cases, the new subgoal is $U$.
If the goal is neither a product nor starting with a let definition,
-the tactic {\tt intro} applies the tactic {\tt red} until the tactic
-{\tt intro} can be applied or the goal is not reducible.
+the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
+{\tt intro} can be applied or the goal is not head-reducible.
\begin{ErrMsgs}
\item \errindex{No product even after head-reduction}
@@ -2916,7 +2916,8 @@ \subsection{\tt hnf}
This tactic applies to any goal. It replaces the current goal with its
head normal form according to the $\beta\delta\iota\zeta$-reduction
rules, i.e. it reduces the head of the goal until it becomes a
-product or an irreducible term.
+product or an irreducible term. All inner $\beta\iota$-redexes are also
+reduced.
\Example
The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
View
@@ -812,7 +812,7 @@ let try_red_product env sigma c =
let red_product env sigma c =
try try_red_product env sigma c
- with Redelimination -> error "Not reducible."
+ with Redelimination -> error "No head constant to reduce."
(*
(* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -882,8 +882,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
| CoFix _ | Fix _ -> s'
| _ -> redrec (applist(c, stack)))
| None -> s'
- else s'
- in applist (redrec c)
+ else s' in
+ let simpfun = clos_norm_flags betaiota env sigma in
+ simpfun (applist (redrec c))
let hnf_constr = whd_simpl_orelse_delta_but_fix
View
@@ -443,9 +443,9 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
(* that intro do betaiotazeta only when reduction is needed; and *)
(* probably also a pity that intro does zeta *)
try
- tclTHEN try_red_in_concl
- (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl
- with Redelimination ->
+ tclTHEN hnf_in_concl
+ (intro_then_gen loc name_flag move_flag false dep_flag tac) gl
+ with RefinerError IntroNeedsProduct ->
user_err_loc(loc,"Intro",str "No product even after head-reduction.")
let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC)
@@ -3,5 +3,22 @@
Goal forall A, A -> True.
intros _ _.
+Abort.
+(* This did not work until March 2013, because of underlying "red" *)
+Goal (fun x => True -> True) 0.
+intro H.
+Abort.
+
+(* This should still work, with "intro" calling "hnf" *)
+Goal (fun f => True -> f 0 = f 0) (fun x => x).
+intro H.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
+
+(* Somewhat related: This did not work until March 2013 *)
+Goal (fun f => f 0 = f 0) (fun x => x).
+hnf.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
@@ -93,21 +93,9 @@ Program Instance all_iff_morphism {A : Type} :
Program Instance all_impl_morphism {A : Type} :
Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
- Next Obligation.
- Proof.
- unfold pointwise_relation, all in *.
- intuition ; specialize (H x0) ; intuition.
- Qed.
-
Program Instance all_inverse_impl_morphism {A : Type} :
Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
- Next Obligation.
- Proof.
- unfold pointwise_relation, all in *.
- intuition ; specialize (H x0) ; intuition.
- Qed.
-
(** Equivalent points are simultaneously accessible or not *)
Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)

0 comments on commit d223f85

Please sign in to comment.