Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 252 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 6bb9e268b2..e4e2a89bd4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,10 +8,18 @@ Tactic Language
 
 - Second-order pattern-matching now working in Ltac "match" clauses
   (syntax for second-order unification variable is "@?X").
+- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer)
+
+Changes from V8.1gamma to V8.1
+==============================
+
+Bug fixes
+
+- Many bugs have been fixed (cf coq-bugs web page)
 
 Tactics
 
-- New tactic ring, ring_simplify and new tactic field now able to manage
+- New tactics ring, ring_simplify and new tactic field now able to manage
   power to a positive integer constant. Tactic ring on Z and R, and
   field on R manage power (may lead to incompatibilities with V8.1gamma).
 - Tactic field_simplify now applicable in hypotheses.
@@ -20,6 +28,12 @@ Tactics
   all able to apply user-given equations to rewrite monoms on the fly 
   (see documentation).
 
+Libraries
+
+- New file ConstructiveEpsilon.v defining an epsilon operator and
+  proving the axiom of choice constructively for a countable domain
+  and a decidable predicate.
+
 Changes from V8.1beta to V8.1gamma
 ==================================
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 8b1c6dfc5c..d79910c99e 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -53,7 +53,7 @@ let cl_sigma ce = evars_of ce.env
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
     templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    env = subst_evar_defs sub clenv.env;
+    env = subst_evar_defs_light sub clenv.env;
     templenv = clenv.templenv }
 
 let clenv_nf_meta clenv c = nf_meta clenv.env c
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 34f5a3c14f..66270c2b31 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -327,7 +327,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | Rigid _, Flexible ev2 ->
@@ -342,7 +342,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | MaybeFlexible flex1, Rigid _ ->
@@ -524,8 +524,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 let consider_remaining_unif_problems env isevars =
   let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
   List.fold_left
-    (fun (isevars,b as p) (pbty,t1,t2) ->
-      (* Pas le bon env pour le problème... *)
+    (fun (isevars,b as p) (pbty,env,t1,t2) ->
       if b then first_order_unification env isevars pbty 
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6f50dc93fe..54e84db86f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -598,7 +598,7 @@ let solve_pattern_eqn env l1 c =
  * ass.
  *)
 
-let status_changed lev (pbty,t1,t2) =
+let status_changed lev (pbty,_,t1,t2) =
   try 
     List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
   with Failure _ ->
@@ -657,7 +657,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  evar_define env ev1 t2 isevars in
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
-      (fun (isevars,b as p) (pbty,t1,t2) ->
+      (fun (isevars,b as p) (pbty,env,t1,t2) ->
 	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2afe4601ff..a247b5b1ef 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -372,18 +372,17 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
 
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_defs =
     { evars : evar_map;
       conv_pbs : evar_constraint list;
       history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
-let subst_evar_defs sub evd =
+let subst_evar_defs_light sub evd =
+  assert (evd.evars = (Evarmap.empty,UniverseMap.empty));
+  assert (evd.conv_pbs = []);
   { evd with
-    conv_pbs =
-      List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2))
-        evd.conv_pbs;
     metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
 
 let create_evar_defs sigma =
@@ -567,7 +566,7 @@ let pr_evar_map sigma =
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+    (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) ->
       print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8b9c7fc677..ac1ed145af 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -120,8 +120,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (* Unification state *)
 type evar_defs
 
-(* Substitution is not applied to the [evar_map] *)
-val subst_evar_defs : substitution -> evar_defs -> evar_defs
+(* Assume empty [evar_map] and [conv_pbs] *)
+val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
 (* create an [evar_defs] with empty meta map: *)
 val create_evar_defs : evar_map -> evar_defs
@@ -147,7 +147,7 @@ val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 (* Unification constraints *)
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
 val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
   evar_defs * evar_constraint list
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
new file mode 100644
index 0000000000..062c3ee5c3
--- /dev/null
+++ b/test-suite/success/conv_pbs.v
@@ -0,0 +1,223 @@
+(* A bit complex but realistic example whose last fixpoint definition
+   used to fail in 8.1 because of wrong environment in conversion
+   problems (see revision 9664) *)
+
+Require Import List.
+Require Import Arith.
+
+Parameter predicate : Set.
+Parameter function : Set.
+Definition variable := nat.
+Definition x0 := 0.
+Definition var_eq_dec := eq_nat_dec.
+
+Inductive term : Set :=
+  | App : function -> term -> term
+  | Var : variable -> term.
+
+Definition atom := (predicate * term)%type.
+
+Inductive formula : Set :=
+  | Atom : atom -> formula
+  | Imply : formula -> formula -> formula
+  | Forall : variable -> formula -> formula.
+
+Notation "A --> B" := (Imply A B) (at level 40).
+
+Definition substitution range := list (variable * range).
+
+Fixpoint remove_assoc (A:Set)(x:variable)(rho: substitution A){struct rho}
+                      : substitution A :=
+  match rho with
+    | nil => rho
+    | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho 
+                      else (y,t) :: remove_assoc A x rho
+  end.
+
+Fixpoint assoc (A:Set)(x:variable)(rho:substitution A){struct rho}
+               : option A :=
+  match rho with
+    | nil => None
+    | (y,t) :: rho => if var_eq_dec x y then Some t 
+                      else assoc A x rho
+  end.
+
+Fixpoint subst_term (rho:substitution term)(t:term){struct t} : term :=
+  match t with
+  | Var x => match assoc _ x rho with
+             | Some a => a
+             | None => Var x
+             end
+  | App f t' => App f (subst_term rho t')
+  end.
+
+Fixpoint subst_formula (rho:substitution term)(A:formula){struct A}:formula :=
+  match A with
+  | Atom (p,t) => Atom (p, subst_term rho t)
+  | A --> B => subst_formula rho A --> subst_formula rho B
+  | Forall y A => Forall y (subst_formula (remove_assoc _ y rho) A)
+  (* assume t closed *)
+  end.
+
+Definition subst A x t := subst_formula ((x,t):: nil) A.
+
+Record Kripke : Type := {
+  worlds: Set;
+  wle : worlds -> worlds -> Type;
+  wle_refl : forall w, wle w w ;
+  wle_trans : forall w w' w'', wle w w' -> wle w' w'' -> wle w w'';
+  domain : Set;
+  vars : variable -> domain;
+  funs : function -> domain -> domain;
+  atoms : worlds -> predicate * domain -> Type;
+  atoms_mon : forall w w', wle w w' -> forall P, atoms w P -> atoms w' P
+}.
+
+Section Sem.
+
+Variable K : Kripke.
+
+Fixpoint sem (rho: substitution (domain K))(t:term){struct t} : domain K :=
+  match t with
+  | Var x => match assoc _ x rho with
+             | Some a => a
+             | None => vars K x
+             end
+  | App f t' => funs K f (sem rho t')
+  end.
+
+End Sem.
+
+Notation "w <= w'" := (wle _ w w').
+
+Set Implicit Arguments.
+
+Reserved Notation "w ||- A" (at level 70).
+
+Definition context := list formula.
+
+Variable fresh : variable -> context -> Prop.
+
+Variable fresh_out : context -> variable.
+
+Axiom fresh_out_spec : forall Gamma, fresh (fresh_out Gamma) Gamma.
+
+Axiom fresh_peel : forall x A Gamma, fresh x (A::Gamma) -> fresh x Gamma.
+
+Fixpoint force (K:Kripke)(rho: substitution (domain K))(w:worlds K)(A:formula)
+               {struct A} : Type :=
+  match A with
+  | Atom (p,t) => atoms K w (p, sem K rho t)
+  | A --> B => forall w', w <= w' -> force K rho w' A -> force K rho w' B
+  | Forall x A => forall w', w <= w' -> forall t, force K ((x,t)::remove_assoc _ x rho) w' A
+  end.
+
+Notation "w ||- A" := (force _ nil w A).
+
+Reserved Notation "Gamma |- A" (at level 70).
+Reserved Notation "Gamma ; A |- C" (at level 70, A at next level).
+
+Inductive context_prefix (Gamma:context) : context -> Type :=
+  | CtxPrefixRefl : context_prefix Gamma Gamma
+  | CtxPrefixTrans : forall A Gamma', context_prefix Gamma Gamma' -> context_prefix Gamma (cons A Gamma').
+
+Inductive in_context (A:formula) : list formula -> Prop :=
+  | InAxiom : forall Gamma, in_context A (cons A Gamma)
+  | OmWeak : forall Gamma B, in_context A Gamma -> in_context A (cons B Gamma).
+
+Inductive prove : list formula -> formula -> Type :=
+  | ProofImplyR : forall A B Gamma, prove (cons A Gamma) B 
+    -> prove Gamma (A --> B)
+  | ProofForallR : forall x A Gamma, (forall y, fresh y (A::Gamma) 
+    -> prove Gamma (subst A x (Var y))) -> prove Gamma (Forall x A)
+  | ProofCont : forall A Gamma Gamma' C, context_prefix (A::Gamma) Gamma' 
+    -> (prove_stoup Gamma' A C) -> (Gamma' |- C)
+
+where "Gamma |- A" := (prove Gamma A)
+
+  with prove_stoup : list formula -> formula -> formula -> Type :=
+  | ProofAxiom Gamma C: Gamma ; C |- C
+  | ProofImplyL Gamma C : forall A B, (Gamma |- A) 
+    -> (prove_stoup Gamma B C) -> (prove_stoup Gamma (A --> B) C)
+  | ProofForallL Gamma C : forall x t A, (prove_stoup Gamma (subst A x t) C) 
+    -> (prove_stoup Gamma (Forall x A) C)
+
+where " Gamma ; B |- A " := (prove_stoup Gamma B A).
+
+Axiom context_prefix_trans : 
+  forall Gamma Gamma' Gamma'',
+    context_prefix Gamma Gamma' 
+      -> context_prefix Gamma' Gamma''
+        -> context_prefix Gamma Gamma''.
+
+Axiom Weakening : 
+  forall Gamma Gamma' A,
+    context_prefix Gamma Gamma' -> Gamma |- A -> Gamma' |- A.
+    
+Axiom universal_weakening :
+  forall Gamma Gamma', context_prefix Gamma Gamma'
+    -> forall P, Gamma |- Atom P -> Gamma' |- Atom P.
+
+Canonical Structure Universal := Build_Kripke
+  context
+  context_prefix
+  CtxPrefixRefl
+  context_prefix_trans
+  term
+  Var
+  App
+  (fun Gamma P => Gamma |- Atom P)
+  universal_weakening.
+
+Axiom subst_commute :
+  forall A rho x t, 
+    subst_formula ((x,t)::rho) A = subst (subst_formula rho A) x t.
+
+Axiom subst_formula_atom :
+  forall rho p t, 
+    Atom (p, sem _ rho t) = subst_formula rho (Atom (p,t)).
+
+Fixpoint universal_completeness (Gamma:context)(A:formula){struct A}
+  : forall rho:substitution term, 
+      force _ rho Gamma A -> Gamma |- subst_formula rho A
+  :=
+  match A 
+    return forall rho, force _ rho Gamma A 
+      -> Gamma |- subst_formula rho A 
+  with
+  | Atom (p,t) => fun rho H => eq_rect _ (fun A => Gamma |- A) H _ (subst_formula_atom rho p t)
+  | A --> B => fun rho HImplyAB =>
+    let A' := subst_formula rho A in
+    ProofImplyR (universal_completeness (A'::Gamma) B rho
+     (HImplyAB (A'::Gamma)(CtxPrefixTrans A' (CtxPrefixRefl Gamma))
+       (universal_completeness_stoup A rho (fun C Gamma' Hle p
+         => ProofCont Hle p))))
+  | Forall x A => fun rho HForallA 
+    => ProofForallR x (fun y Hfresh 
+      => eq_rect _ _ (universal_completeness Gamma A _ 
+        (HForallA Gamma (CtxPrefixRefl Gamma)(Var y))) _ (subst_commute _ _ _ _ ))
+  end
+with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
+  : forall rho, (forall C Gamma', context_prefix Gamma Gamma'
+    -> Gamma' ; subst_formula rho A |- C -> Gamma' |- C)
+      -> force _ rho Gamma A
+  := 
+  match A return forall rho, 
+    (forall C Gamma', context_prefix Gamma Gamma' 
+     -> Gamma' ; subst_formula rho A |- C
+     -> Gamma' |- C)
+       -> force _ rho Gamma A 
+  with
+  | Atom (p,t) as C => fun rho H
+    => H _ Gamma (CtxPrefixRefl Gamma)(ProofAxiom _ _)
+  | A --> B => fun rho H => fun Gamma' Hle HA
+    => universal_completeness_stoup B rho (fun C Gamma'' Hle' p
+      => H C Gamma'' (context_prefix_trans Hle Hle')
+         (ProofImplyL (Weakening Hle' (universal_completeness Gamma' A rho HA)) p))
+  | Forall x A => fun rho H => fun Gamma' Hle t
+    => (universal_completeness_stoup A ((x,t)::remove_assoc _ x rho)
+        (fun C Gamma'' Hle' p =>
+          H C Gamma'' (context_prefix_trans Hle Hle')
+          (ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
+          (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
+  end.