Lemma foo (H : forall A, A) : forall A, A. Show Universes. eexact H. Qed. (* File reduced by coq-bug-finder from original input, then from 6390 lines to 397 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 17 2015 12:34:25 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (1b3759e78f227eb85a128c58b8ce8c11509dd8c3) *) Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. Require Import Coq.Lists.SetoidList. Require Export Coq.Program.Program. Global Set Implicit Arguments. Global Set Asymmetric Patterns. Fixpoint combine_sig_helper {T} {P : T -> Prop} (ls : list T) : (forall x, In x ls -> P x) -> list (sig P). admit. Defined. Lemma Forall_forall1_transparent_helper_1 {A P} {x : A} {xs : list A} {l : list A} (H : Forall P l) (H' : x::xs = l) : P x. admit. Defined. Lemma Forall_forall1_transparent_helper_2 {A P} {x : A} {xs : list A} {l : list A} (H : Forall P l) (H' : x::xs = l) : Forall P xs. admit. Defined. Fixpoint Forall_forall1_transparent {A} (P : A -> Prop) (l : list A) {struct l} : Forall P l -> forall x, In x l -> P x := match l as l return Forall P l -> forall x, In x l -> P x with | nil => fun _ _ f => match f : False with end | x::xs => fun H x' H' => match H' with | or_introl H'' => eq_rect x P (Forall_forall1_transparent_helper_1 H eq_refl) _ H'' | or_intror H'' => @Forall_forall1_transparent A P xs (Forall_forall1_transparent_helper_2 H eq_refl) _ H'' end end. Definition combine_sig {T P ls} (H : List.Forall P ls) : list (@sig T P) := combine_sig_helper ls (@Forall_forall1_transparent T P ls H). 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. Record string_like (CharType : Type) := { String :> Type; Singleton : CharType -> String where "[ x ]" := (Singleton x); Empty : String; Concat : String -> String -> String where "x ++ y" := (Concat x y); bool_eq : String -> String -> bool; bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y; Length : String -> nat; Associativity : forall x y z, (x ++ y) ++ z = x ++ (y ++ z); LeftId : forall x, Empty ++ x = x; RightId : forall x, x ++ Empty = x; Singleton_Length : forall x, Length (Singleton x) = 1; Length_correct : forall s1 s2, Length s1 + Length s2 = Length (s1 ++ s2); Length_Empty : Length Empty = 0; Empty_Length : forall s1, Length s1 = 0 -> s1 = Empty; Not_Singleton_Empty : forall x, Singleton x <> Empty; SplitAt : nat -> String -> String * String; SplitAt_correct : forall n s, fst (SplitAt n s) ++ snd (SplitAt n s) = s; SplitAt_concat_correct : forall s1 s2, SplitAt (Length s1) (s1 ++ s2) = (s1, s2); SplitAtLength_correct : forall n s, Length (fst (SplitAt n s)) = min (Length s) n }. Delimit Scope string_like_scope with string_like. Bind Scope string_like_scope with String. Arguments Length {_%type_scope _} _%string_like. Notation "[[ x ]]" := (@Singleton _ _ x) : string_like_scope. Infix "++" := (@Concat _ _) : string_like_scope. Infix "=s" := (@bool_eq _ _) (at level 70, right associativity) : string_like_scope. Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String) := Length s1 < Length s2 \/ s1 = s2. Infix "≤s" := str_le (at level 70, right associativity). Record StringWithSplitState {CharType} (String : string_like CharType) (split_stateT : String -> Type) := { string_val :> String; state_val : split_stateT string_val }. Module Export ContextFreeGrammar. Require Import Coq.Strings.String. Section cfg. Variable CharType : Type. Section definitions. Inductive item := | Terminal (_ : CharType) | 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. End cfg. End ContextFreeGrammar. Module Export BaseTypes. Import Coq.Strings.String. Local Open Scope string_like_scope. Inductive any_grammar CharType := | include_item (_ : item CharType) | include_production (_ : production CharType) | include_productions (_ : productions CharType) | include_nonterminal (_ : string). Global Coercion include_item : item >-> any_grammar. Global Coercion include_production : production >-> any_grammar. Section recursive_descent_parser. Context {CharType : Type} {String : string_like CharType} {G : grammar CharType}. Class parser_computational_predataT := { nonterminals_listT : Type; initial_nonterminals_data : nonterminals_listT; is_valid_nonterminal : nonterminals_listT -> string -> bool; remove_nonterminal : nonterminals_listT -> string -> nonterminals_listT; nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; remove_nonterminal_dec : forall ls nonterminal, is_valid_nonterminal ls nonterminal = true -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; ntl_wf : well_founded nonterminals_listT_R }. Class parser_computational_types_dataT := { predata :> parser_computational_predataT; split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }. Class parser_computational_dataT' `{parser_computational_types_dataT} := { split_string_for_production : forall (str0 : String) (valid : nonterminals_listT) (it : item CharType) (its : production CharType) (str : StringWithSplitState String (split_stateT str0 valid (it::its : production CharType))), list (StringWithSplitState String (split_stateT str0 valid it) * StringWithSplitState String (split_stateT str0 valid its)); split_string_for_production_correct : forall str0 valid it its str, let P f := List.Forall f (@split_string_for_production str0 valid it its str) in P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true) }. End recursive_descent_parser. End BaseTypes. Import Coq.Strings.String. Section cfg. Context CharType (String : string_like CharType) (G : grammar CharType). Context (names_listT : Type) (initial_names_data : names_listT) (is_valid_name : names_listT -> string -> bool) (remove_name : names_listT -> string -> names_listT) (names_listT_R : names_listT -> names_listT -> Prop) (remove_name_dec : forall ls name, is_valid_name ls name = true -> names_listT_R (remove_name ls name) ls) (remove_name_1 : forall ls ps ps', is_valid_name (remove_name ls ps) ps' = true -> is_valid_name ls ps' = true) (remove_name_2 : forall ls ps ps', is_valid_name (remove_name ls ps) ps' = false <-> is_valid_name ls ps' = false \/ ps = ps') (ntl_wf : well_founded names_listT_R). Inductive minimal_parse_of : forall (str0 : String) (valid : names_listT) (str : String), productions CharType -> 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 : names_listT) (str : String), production CharType -> Type := | MinParseProductionNil : forall str0 valid, @minimal_parse_of_production str0 valid (Empty _) nil | MinParseProductionCons : forall str0 valid str strs pat pats, str ++ strs ≤s str0 -> @minimal_parse_of_item str0 valid str pat -> @minimal_parse_of_production str0 valid strs pats -> @minimal_parse_of_production str0 valid (str ++ strs) (pat::pats) with minimal_parse_of_item : forall (str0 : String) (valid : names_listT) (str : String), item CharType -> Type := | MinParseTerminal : forall str0 valid x, @minimal_parse_of_item str0 valid [[ x ]]%string_like (Terminal x) | MinParseNonTerminal : forall str0 valid str name, @minimal_parse_of_name str0 valid str name -> @minimal_parse_of_item str0 valid str (NonTerminal CharType name) with minimal_parse_of_name : forall (str0 : String) (valid : names_listT) (str : String), string -> Type := | MinParseNonTerminalStrLt : forall str0 valid name str, Length str < Length str0 -> is_valid_name initial_names_data name = true -> @minimal_parse_of str initial_names_data str (Lookup G name) -> @minimal_parse_of_name str0 valid str name | MinParseNonTerminalStrEq : forall str valid name, is_valid_name initial_names_data name = true -> is_valid_name valid name = true -> @minimal_parse_of str (remove_name valid name) str (Lookup G name) -> @minimal_parse_of_name str valid str name. End cfg. Local Coercion is_true : bool >-> Sortclass. Local Open Scope string_like_scope. Section general. Context {CharType} {String : string_like CharType} {G : grammar CharType}. Class boolean_parser_dataT := { predata :> parser_computational_predataT; split_stateT : String -> Type; data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |}; split_string_for_production : forall it its, StringWithSplitState String split_stateT -> list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT); split_string_for_production_correct : forall it its (str : StringWithSplitState String split_stateT), let P f := List.Forall f (split_string_for_production it its str) in P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true); premethods :> parser_computational_dataT' := @Build_parser_computational_dataT' _ String data' (fun _ _ => split_string_for_production) (fun _ _ => split_string_for_production_correct) }. Definition split_list_completeT `{data : boolean_parser_dataT} {str0 valid} (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) (split_list : list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT)) (it : item CharType) (its : production CharType) := ({ s1s2 : String * String & (fst s1s2 ++ snd s1s2 =s str) * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type) -> ({ s1s2 : StringWithSplitState String split_stateT * StringWithSplitState String split_stateT & (In s1s2 split_list) * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type). End general. Section recursive_descent_parser. Context {CharType} {String : string_like CharType} {G : grammar CharType}. Context `{data : @boolean_parser_dataT _ String}. Section bool. Section parts. Definition parse_item (str_matches_nonterminal : string -> bool) (str : StringWithSplitState String split_stateT) (it : item CharType) : bool := match it with | Terminal ch => [[ ch ]] =s str | NonTerminal nt => str_matches_nonterminal nt end. Section production. Context {str0} (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), str ≤s str0 -> string -> bool). Fixpoint parse_production (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) (prod : production CharType) : bool. Proof. refine match prod with | nil => str =s Empty _ | it::its => let parse_production' := fun str pf => parse_production str pf its in fold_right orb false (let mapF f := map f (combine_sig (split_string_for_production_correct it its str)) in mapF (fun s1s2p => (parse_item (parse_nonterminal (fst (proj1_sig s1s2p)) _) (fst (proj1_sig s1s2p)) it) && parse_production' (snd (proj1_sig s1s2p)) _)%bool) end; revert pf; clear; intros; admit. Defined. End production. End parts. End bool. End recursive_descent_parser. Section sound. Context CharType (String : string_like CharType) (G : grammar CharType). Context `{data : @boolean_parser_dataT CharType String}. Section production. Context (str0 : String) (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), str ≤s str0 -> string -> bool). Definition parse_nonterminal_completeT P := forall valid (str : StringWithSplitState String split_stateT) pf nonterminal (H_sub : P str0 valid nonterminal), minimal_parse_of_name _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal -> @parse_nonterminal str pf nonterminal = true. Lemma parse_production_complete valid Pv (parse_nonterminal_complete : parse_nonterminal_completeT Pv) (Hinit : forall str (pf : str ≤s str0) nonterminal, minimal_parse_of_name String G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal -> Pv str0 valid nonterminal) (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) (prod : production CharType) (split_string_for_production_complete' : forall str0 valid str pf, Forall_tails (fun prod' => match prod' return Type with | nil => True | it::its => split_list_completeT (G := G) (valid := valid) (str0 := str0) str pf (split_string_for_production it its str) it its end) prod) : minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str prod -> parse_production parse_nonterminal str pf prod = true. admit. Defined. End production. Context (str0 : String) (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), str ≤s str0 -> string -> bool). Goal forall (a : production CharType), (forall (str1 : String) (valid : nonterminals_listT) (str : StringWithSplitState String split_stateT) (pf : str ≤s str1), Forall_tails (fun prod' : list (item CharType) => match prod' with | [] => True | it :: its => split_list_completeT (G := G) (valid := valid) str pf (split_string_for_production it its str) it its end) a) -> forall (str : String) (pf : str ≤s str0) (st : split_stateT str), parse_production parse_nonterminal {| string_val := str; state_val := st |} pf a = true. Proof. intros a X **. eapply parse_production_complete. Focus 3. exact X. Undo. assumption. Undo. eassumption. (* no applicable tactic *)