|
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 *)
Abort.
End sound.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
