diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 13 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 5 | ||||
| -rw-r--r-- | library/impargs.ml | 3 | ||||
| -rw-r--r-- | library/impargs.mli | 12 | ||||
| -rw-r--r-- | ltac/ltac.mllib | 1 | ||||
| -rw-r--r-- | ltac/profile_ltac.ml | 2 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 13 | ||||
| -rw-r--r-- | ltac/taccoerce.ml (renamed from tactics/taccoerce.ml) | 0 | ||||
| -rw-r--r-- | ltac/taccoerce.mli (renamed from tactics/taccoerce.mli) | 0 | ||||
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 11 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4187.v | 709 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4653.v | 3 | ||||
| -rw-r--r-- | test-suite/success/Case13.v | 8 | ||||
| -rw-r--r-- | test-suite/success/programequality.v | 13 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 8 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 5 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 1 | ||||
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 2 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 30 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 1 |
25 files changed, 779 insertions, 75 deletions
@@ -13,6 +13,7 @@ Bugfixes - #4592, #4932: notations sharing recursive patterns or sharing binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #3070: fixing "subst" in the presence of a chain of dependencies. Specification language @@ -625,6 +626,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1163,9 +1167,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5ba3c308a..9fbff7181 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1277,7 +1277,7 @@ Prints the profile Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. \begin{quote} -{\tt Reset Profile}. +{\tt Reset Ltac Profile}. \end{quote} Resets the profile, that is, deletes all accumulated information diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c4688f9f..30016dedc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1078,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1094,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 931fc1ca4..1e14eeb81 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e2110..bce7a15cb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicit_protection f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt diff --git a/library/impargs.mli b/library/impargs.mli index 34e529ca2..3919a519c 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 65ed114cf..fc51e48ae 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Taccoerce Tacsubst Tacenv Tactic_debug diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index f332e1a0d..bea02e3dc 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -139,7 +139,7 @@ let string_of_call ck = let s = string_of_ppcmds (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 47c78ae5c..7acad20d2 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1440,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy = fun ({ state = () } as input) -> let unify env evars t = let (sigma, cstrs) = evars in - let ans = - try Some (refresh_hypinfo env sigma c) - with e when Class_tactics.catchable e -> None - in - match ans with - | None -> None - | Some (sigma, rew) -> - let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in - match rew with - | None -> None - | Some rew -> Some rew + let (sigma, rew) = refresh_hypinfo env sigma c in + unify_eqn rew l2r flags env (sigma, cstrs) None t in let app = apply_rule unify occs in let strat = diff --git a/tactics/taccoerce.ml b/ltac/taccoerce.ml index 0110510d3..0110510d3 100644 --- a/tactics/taccoerce.ml +++ b/ltac/taccoerce.ml diff --git a/tactics/taccoerce.mli b/ltac/taccoerce.mli index 0b67f8726..0b67f8726 100644 --- a/tactics/taccoerce.mli +++ b/ltac/taccoerce.mli diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487..fe2b0a5a1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c97cf442..3e5b7b65f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -629,7 +629,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 38af9a0ca..acc0fa1ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1270,7 +1270,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac @@ -4865,8 +4865,13 @@ let abstract_subproof id gk tac = in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in - (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 48722f655..093302608 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -12,7 +12,6 @@ Equality Contradiction Inv Leminv -Taccoerce Hints Auto Eauto diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 000000000..b13ca36a3 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 000000000..4514342c5 --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8e..8f95484cf 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v new file mode 100644 index 000000000..414c572f8 --- /dev/null +++ b/test-suite/success/programequality.v @@ -0,0 +1,13 @@ +Require Import Program. + +Axiom t : nat -> Set. + +Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type) + (a : t x), + P (eq_rect _ _ a _ e) e'. +Proof. + intros. + pi_eq_proofs. clear e. + destruct e'. simpl. + change (P a eq_refl). +Abort.
\ No newline at end of file diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c45889479..80b0b7e4c 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1. -Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1. -Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. Next Obligation. Proof. intros A R sa x y z Hxy Hyz. @@ -123,7 +123,7 @@ Section Respecting. End Respecting. -(** The default equivalence on function spaces, with higher-priority than [eq]. *) +(** The default equivalence on function spaces, with higher priority than [eq]. *) Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : Reflexive (pointwise_relation A eqB) | 9. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index a349eb908..d6f9bb9df 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -8,7 +8,6 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Export ProofIrrelevance. Require Export JMeq. Require Import Coq.Program.Tactics. @@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p := | [ H : X = Y |- _ ] => match p with | H => fail 2 - | _ => rewrite (proof_irrelevance (X = Y) p H) + | _ => rewrite (UIP _ X Y p H) end | _ => fail " No hypothesis with same type " end @@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. apply proof_irrelevance. Qed. +Proof. apply UIP. Qed. Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c8f37318d..2a3ec926b 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,6 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. +Require Export ProofIrrelevance. Local Open Scope program_scope. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442e..d43baee8c 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 005ffdae7..919f37b91 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -675,7 +675,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -736,24 +736,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -763,6 +746,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -771,10 +758,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b3eae3765..ff4c18ad2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,6 +320,7 @@ let explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e |