in the dependently typed case; not including discrimination of cycles).
-content.cmi:
acic2content.cmi: content.cmi
content2cic.cmi: content.cmi
cicNotationUtil.cmi: cicNotationPt.cmx
cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
acic2astMatcher.cmi: cicNotationPt.cmx
termAcicContent.cmi: cicNotationPt.cmx
-cicNotationPt.cmo:
-cicNotationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
acic2content.cmo: content.cmi acic2content.cmi
-proceduralHelpers.cmi:
-proceduralClassify.cmi:
-proceduralOptimizer.cmi:
-proceduralTypes.cmi:
-proceduralMode.cmi:
-proceduralConversion.cmi:
procedural1.cmi: proceduralTypes.cmi
procedural2.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
-acic2Procedural.cmi:
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralHelpers.cmx: proceduralHelpers.cmi
proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi
-extractor.cmo:
-extractor.cmx:
-extractor_manager.cmo:
-extractor_manager.cmx:
-table_creator.cmo:
-table_creator.cmx:
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
-cicUniv.cmi:
unshare.cmi: cic.cmx
deannotate.cmi: cic.cmx
cicParser.cmi: cic.cmx
cicUtil.cmi: cic.cmx
helmLibraryObjects.cmi: cic.cmx
-libraryObjects.cmi:
cic_indexable.cmi: cic.cmx
path_indexing.cmi: cic.cmx
cicInspect.cmi: cic.cmx
-eta_fixing.cmi:
-doubleTypeInference.cmi:
-cic2acic.cmi:
cic2Xml.cmi: cic2acic.cmi
eta_fixing.cmo: eta_fixing.cmi
eta_fixing.cmx: eta_fixing.cmi
-cicDisambiguate.cmi:
-disambiguateChoices.cmi:
cicDisambiguate.cmo: cicDisambiguate.cmi
cicDisambiguate.cmx: cicDisambiguate.cmi
disambiguateChoices.cmo: disambiguateChoices.cmi
-cicExportation.cmi:
cicExportation.cmo: cicExportation.cmi
cicExportation.cmx: cicExportation.cmi
-cicLogger.cmi:
-cicEnvironment.cmi:
-cicPp.cmi:
-cicUnivUtils.cmi:
-cicSubstitution.cmi:
-cicMiniReduction.cmi:
-cicReduction.cmi:
-cicTypeChecker.cmi:
-freshNamesGenerator.cmi:
-cicDischarge.cmi:
cicLogger.cmo: cicLogger.cmi
cicLogger.cmx: cicLogger.cmi
cicEnvironment.cmo: cicEnvironment.cmi
-cicMetaSubst.cmi:
-cicMkImplicit.cmi:
-termUtil.cmi:
-coercGraph.cmi:
-cicUnification.cmi:
-cicReplace.cmi:
-cicRefine.cmi:
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
-renderingAttrs.cmi:
-cicNotationLexer.cmi:
-cicNotationParser.cmi:
-mpresentation.cmi:
-box.cmi:
-content2presMatcher.cmi:
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
cicNotationPres.cmi: mpresentation.cmi box.cmi
-disambiguateTypes.cmi:
disambiguate.cmi: disambiguateTypes.cmi
multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
-componentsConf.cmi:
-hExtlib.cmi:
-hMarshal.cmi:
-patternMatcher.cmi:
-hLog.cmi:
-trie.cmi:
-discrimination_tree.cmi:
-hTopoSort.cmi:
-refCounter.cmi:
-graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
hExtlib.cmo: hExtlib.cmi
-http_getter_wget.cmi:
-http_getter_logger.cmi:
-http_getter_misc.cmi:
-http_getter_const.cmi:
http_getter_env.cmi: http_getter_types.cmx
-http_getter_storage.cmi:
http_getter_common.cmi: http_getter_types.cmx
http_getter.cmi: http_getter_types.cmx
-http_getter_types.cmo:
-http_getter_types.cmx:
http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi
http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
http_getter_logger.cmo: http_getter_logger.cmi
grafiteAstPp.cmi: grafiteAst.cmx
grafiteMarshal.cmi: grafiteAst.cmx
-grafiteAst.cmo:
-grafiteAst.cmx:
grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi
| NChange of loc * npattern * CicNotationPt.term
| NConstructor of loc * int option * CicNotationPt.term list
| NCut of loc * CicNotationPt.term
+(* | NDiscriminate of loc * CicNotationPt.term
+ | NSubst of loc * CicNotationPt.term *)
+ | NDestruct of loc
| NElim of loc * CicNotationPt.term * npattern
| NGeneralize of loc * npattern
| NId of loc
| NBranch of loc
| NShift of loc
| NPos of loc * int list
+ | NPosbyname of loc * string
| NWildcard of loc
| NMerge of loc
| NSkip of loc
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 30
+let magic = 33
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
type ncommand =
| UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
| NObj of loc * CicNotationPt.term CicNotationPt.obj
+ | NDiscriminator of loc * CicNotationPt.term
| NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option
| NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
+(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
+ | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
+ | NDestruct _ -> "ndestruct"
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NBranch _ -> "##["
| NShift _ -> "##|"
| NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+ | NPosbyname (_, s) -> "##" ^ s ^ ":"
| NWildcard _ -> "##*:"
| NMerge _ -> "##]"
| NFocus (_,l) ->
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NDiscriminator (_,_)
| NInverter (_,_,_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
-grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
nCicCoercDeclaration.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
NTactics.constructor_tac
?num ~args:(List.map (fun x -> text,prefix_len,x) args)
| GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
+(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
+ | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+ | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
~what:(text,prefix_len,what) name
| GrafiteAst.NMerge _ -> NTactics.merge_tac
| GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
+ | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
| GrafiteAst.NReduce (_loc, reduction, where) ->
NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
| GrafiteAst.NRewrite (_loc,dir,what,where) ->
[] ->
eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,`New [])
+ | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
+ if status#ng_mode <> `CommandMode then
+ raise (GrafiteTypes.Command_error "Not in command mode")
+ else
+ let status = status#set_ng_mode `ProofMode in
+ let metasenv,subst,status,indty =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+ let indtyno, (_,_,tys,_,_) = match indty with
+ NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
+ indtyno, NCicEnvironment.get_checked_indtys r
+ | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
+ let it = List.nth tys indtyno in
+ let status,obj = NDestructTac.mk_discriminator it status in
+ let _,_,menv,_,_ = obj in
+ (match menv with
+ [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> prerr_endline ("Discriminator: non empty metasenv");
+ status, `New []) *)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
-dependenciesParser.cmi:
-grafiteParser.cmi:
-cicNotation2.cmi:
-nEstatus.cmi:
grafiteDisambiguate.cmi: nEstatus.cmi
-print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
G.NConstructor (loc,
(match num with None -> None | Some x -> Some (int_of_string x)),l)
| IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
+(* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
+ | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
+ | IDENT "ndestruct" -> G.NDestruct loc
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
G.NElim (loc, what, where)
| IDENT "ngeneralize"; p=pattern_spec ->
| SYMBOL "|" -> G.NShift loc
| i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
| SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
+ | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
| SYMBOL "]" -> G.NMerge loc
| SYMBOL ";" -> G.NSemicolon loc
| SYMBOL "." -> G.NDot loc
G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
+ | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
| IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
paramspec = OPT inverter_param_list ;
outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
-domMisc.cmi:
-xml2Gdome.cmi:
domMisc.cmo: domMisc.cmi
domMisc.cmx: domMisc.cmi
xml2Gdome.cmo: xml2Gdome.cmi
-hSql.cmi:
-hSqlite3.cmo:
-hSqlite3.cmx:
-hMysql.cmo:
-hMysql.cmx:
hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi
hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi
cicNotation.cmi: lexiconAst.cmx
lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi
lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx
-lexiconAst.cmo:
-lexiconAst.cmx:
lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi
lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi
-librarian.cmi:
-libraryMisc.cmi:
-libraryDb.cmi:
-coercDb.cmi:
cicCoercion.cmi: coercDb.cmi
-librarySync.cmi:
-cicElim.cmi:
-cicRecord.cmi:
-cicFix.cmi:
-libraryClean.cmi:
librarian.cmo: librarian.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
-helmLogger.cmi:
helmLogger.cmo: helmLogger.cmi
helmLogger.cmx: helmLogger.cmi
-sqlStatements.cmi:
-metadataTypes.cmi:
metadataExtractor.cmi: metadataTypes.cmi
metadataPp.cmi: metadataTypes.cmi
metadataConstraints.cmi: metadataTypes.cmi
-ncic2astMatcher.cmi:
-nTermCicContent.cmi:
ncic2astMatcher.cmo: ncic2astMatcher.cmi
ncic2astMatcher.cmx: ncic2astMatcher.cmi
nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi
-nCicDisambiguate.cmi:
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
-nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmo
nCicSubstitution.cmi: nCic.cmo
-nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmx
nCicSubstitution.cmi: nCic.cmx
val are_all_occurrences_positive:
subst:NCic.substitution ->
NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool
+
+val does_not_occur :
+ subst:NCic.substitution ->
+ ('a * NCic.context_entry) list -> int -> int -> NCic.term -> bool
-nCic2OCic.cmi:
-oCic2NCic.cmi:
-nCicLibrary.cmi:
nCic2OCic.cmo: nCic2OCic.cmi
nCic2OCic.cmx: nCic2OCic.cmi
oCic2NCic.cmo: oCic2NCic.cmi
-nCic2OCic.cmi:
-oCic2NCic.cmi:
-nCicLibrary.cmi:
nCic2OCic.cmo: nCic2OCic.cmi
nCic2OCic.cmx: nCic2OCic.cmi
oCic2NCic.cmo: oCic2NCic.cmi
-terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
orderings.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
nCicProof.cmi: terms.cmi
-nCicParamod.cmi:
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
-nDiscriminationTree.cmi:
-nCicMetaSubst.cmi:
-nCicUnifHint.cmi:
nCicCoercion.cmi: nCicUnifHint.cmi
nRstatus.cmi: nCicCoercion.cmi
nCicUnification.cmi: nRstatus.cmi
-nCicTacReduction.cmi:
-nTacStatus.cmi:
-nCicElim.cmi:
nTactics.cmi: nTacStatus.cmi
-zipTree.cmi:
-andOrTree.cmi:
+andOrTree.cmi: zipTree.cmi
nAuto.cmi: nTacStatus.cmi
nInversion.cmi: nTacStatus.cmi
+nDestructTac.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
zipTree.cmx: zipTree.cmi
andOrTree.cmo: zipTree.cmi andOrTree.cmi
andOrTree.cmx: zipTree.cmx andOrTree.cmi
-nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi
-nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi
+nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi
+nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi
nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi
nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi
+nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi
+nDestructTac.cmx: nTactics.cmx nTacStatus.cmx nDestructTac.cmi
-nCicTacReduction.cmi:
-nTacStatus.cmi:
-nCicElim.cmi:
nTactics.cmi: nTacStatus.cmi
-zipTree.cmi:
-andOrTree.cmi:
+andOrTree.cmi: zipTree.cmi
nAuto.cmi: nTacStatus.cmi
nInversion.cmi: nTacStatus.cmi
+nDestructTac.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
zipTree.cmx: zipTree.cmi
andOrTree.cmo: zipTree.cmi andOrTree.cmi
andOrTree.cmx: zipTree.cmx andOrTree.cmi
-nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi
-nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi
+nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi
+nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi
nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi
nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi
+nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi
+nDestructTac.cmx: nTactics.cmx nTacStatus.cmx nDestructTac.cmi
zipTree.mli \
andOrTree.mli \
nAuto.mli \
- nInversion.mli
+ nInversion.mli \
+ nDestructTac.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_goalty")
;;
+let get_subst status =
+ let _,_,_,subst,_ = status#obj in subst
+;;
+
let to_subst status i entry =
let name,height,metasenv,subst,obj = status#obj in
let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
val metas_of_term : #pstatus as 'status -> cic_term -> int list
val get_goalty: #pstatus -> int -> cic_term
+val get_subst: #pstatus -> NCic.substitution
val mk_meta:
#pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
[ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
| [] -> assert false
| (g, t, k, tag) :: s ->
match init_pos g with (* TODO *)
- | [] | [ _ ] -> fail (lazy "too few goals to branch");
+ | [] | [ _ ] -> fail (lazy "too few goals to branch")
| loc :: loc_tl ->
([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
in
}
;;
+let ref_of_indtyinfo iti = iti.reference;;
+
let analyze_indty_tac ~what indtyref =
distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
's NTacStatus.tactic
val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
+val clear_tac : string list -> 's NTacStatus.tactic
val reduce_tac:
reduction:[ `Normalize of bool | `Whd of bool ] ->
where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
val constructor_tac :
?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic
+
+val atomic_tac :
+ (((int * Continuationals.Stack.switch) list * 'a list * 'b list *
+ [> `NoTag ])
+ list NTacStatus.status ->
+ (< auto_cache : NCicLibrary.automation_cache;
+ coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list;
+ lstatus : LexiconEngine.lexicon_status; obj : NCic.obj;
+ set_coerc_db : NCicCoercion.db -> 'c;
+ set_coercion_status : 'd. (#NCicCoercion.g_status as 'd) -> 'c;
+ set_uhint_db : NCicUnifHint.db -> 'c;
+ set_unifhint_status : 'e. (#NCicUnifHint.g_status as 'e) -> 'c;
+ timestamp : NCicLibrary.timestamp; uhint_db : NCicUnifHint.db; .. >
+ as 'c)) ->
+ (#NTacStatus.tac_status as 'f) -> 'f
+
+type indtyinfo
+
+val ref_of_indtyinfo : indtyinfo -> NReference.reference
+
+val analyze_indty_tac :
+ what:NTacStatus.tactic_term ->
+ indtyinfo option ref -> (#NTacStatus.tac_status as 'a) -> 'a
+
+
+val find_in_context : 'a -> ('a * 'b) list -> int
-helm_registry.cmi:
helm_registry.cmo: helm_registry.cmi
helm_registry.cmx: helm_registry.cmi
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
-proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
-proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
-hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
-universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
-autoCache.cmi:
-paramodulation/utils.cmi:
-closeCoercionGraph.cmi:
-paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
auto.cmi: proofEngineTypes.cmi automationCache.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
-inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
-fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
-history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi
declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi
-threadSafe.cmi:
-extThread.cmi:
threadSafe.cmo: threadSafe.cmi
threadSafe.cmx: threadSafe.cmi
extThread.cmo: extThread.cmi
parser.cmi: ast.cmx
-tptp2grafite.cmi:
-ast.cmo:
-ast.cmx:
lexer.cmo: parser.cmi
lexer.cmx: parser.cmx
parser.cmo: ast.cmx parser.cmi
-uriManager.cmi:
uriManager.cmo: uriManager.cmi
uriManager.cmx: uriManager.cmi
-whelp.cmi:
-fwdQueries.cmi:
whelp.cmo: whelp.cmi
whelp.cmx: whelp.cmi
fwdQueries.cmo: fwdQueries.cmi
-xml.cmi:
-xmlPushParser.cmi:
xml.cmo: xml.cmi
xml.cmx: xml.cmi
xmlPushParser.cmo: xmlPushParser.cmi
-xmlDiff.cmi:
xmlDiff.cmo: xmlDiff.cmi
xmlDiff.cmx: xmlDiff.cmi
applyTransformation.cmo: applyTransformation.cmi
applyTransformation.cmx: applyTransformation.cmi
-buildTimeConf.cmo:
-buildTimeConf.cmx:
dump_moo.cmo: buildTimeConf.cmo
dump_moo.cmx: buildTimeConf.cmx
lablGraphviz.cmo: lablGraphviz.cmi
matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
-matitaGeneratedGui.cmo:
-matitaGeneratedGui.cmx:
matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \
matitaGtkMisc.cmi
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi
virtuals.cmo: virtuals.cmi
virtuals.cmx: virtuals.cmi
-applyTransformation.cmi:
-lablGraphviz.cmi:
-matitaAutoGui.cmi:
-matitaclean.cmi:
-matitacLib.cmi:
-matitadep.cmi:
-matitaEngine.cmi:
-matitaExcPp.cmi:
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo
-matitaInit.cmi:
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi:
matitaScript.cmi: matitaTypes.cmi
-matitaTypes.cmi:
-predefined_virtuals.cmi:
-virtuals.cmi:
-Fsub/part1a_inversion.ma Fsub/defn.ma
Fsub/part1a.ma Fsub/defn.ma
-Fsub/defn.ma Fsub/util.ma
Fsub/util.ma list/in.ma list/list.ma logic/equality.ma nat/compare.ma
-Fsub/part1a_inversion2.ma Fsub/defn2.ma
-Fsub/defn2.ma Fsub/util.ma
+Fsub/defn.ma Fsub/util.ma
+Fsub/adeq.ma Fsub/part1a.ma
+Fsub/part1adb.ma Fsub/defndb.ma nat/le_arith.ma nat/lt_arith.ma
+Fsub/defndb.ma Fsub/util.ma nat/le_arith.ma nat/lt_arith.ma
list/in.ma
list/list.ma
logic/equality.ma
nat/compare.ma
+nat/le_arith.ma
+nat/lt_arith.ma
<keyword>nchange</keyword>
<keyword>nrewrite</keyword>
<keyword>ncut</keyword>
- <keyword>nlapply</keyword>
+ <keyword>nlapply</keyword>
+ <keyword>ndestruct</keyword>
</keyword-list>
<keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-(*
-include "nat/nat.ma".
-include "list/list.ma".
-
-inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
-| il_s : ∀n.T n → index_list T n n
-| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
-
-lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
- ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
-intros 5;elim i
-[destruct;apply il_s;apply f;assumption
-|apply il_c
- [apply f;rewrite > H;assumption
- |apply f1
- [rewrite > H;reflexivity
- |assumption]]]
-qed.
-
-definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
- λT0:Type.λT1:T0 → Type.
- λa0,b0:T0.
- λe0:a0 = b0.
- λso:T1 a0.
- eq_rect' ?? (λy,p.T1 y) so ? e0.
- *)
include "logic/equality.ma".
+
+(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
+ ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
+#T;#a;#b;#e;#P;#H;
+nrewrite < e;*)
+
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
ndefinition R1 ≝ eq_rect_Type0.
+
ndefinition R2 :
∀T0:Type[0].
∀a0:T0.
∀T1:∀x0:T0. a0=x0 → Type[0].
∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
- ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
napply (eq_rect_Type0 ????? e1);
napply (R1 ?? ? ?? e0);
-napply H;
+napply a2;
nqed.
ndefinition R3 :
∀a0:T0.
∀T1:∀x0:T0. a0=x0 → Type[0].
∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
- ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
- ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
+ ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+ ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+ ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ? a0 ? a1 ? e0 = b1.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
- ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
+ ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ??? e0 ? e1);
-napply H;
-nqed.
\ No newline at end of file
+napply (R2 ?? ? ???? e0 ? e1);
+napply a3;
+nqed.
+
+(* include "nat/nat.ma".
+
+ninductive nlist : nat → Type[0] ≝
+| nnil : nlist O
+| ncons : ∀n:nat.nat → nlist n → nlist (S n).
+
+ninductive wrapper : Type[0] ≝
+| kw1 : ∀x.∀y:nlist x.wrapper
+| kw2 : ∀x.∀y:nlist x.wrapper.
+
+nlemma fie : ∀a,b,c,d.∀e:eq ? (kw1 a b) (kw1 c d).
+ ∀P:(∀x1.∀x2:nlist x1. ∀y1.∀y2:nlist y1.eq ? (kw1 x1 x2) (kw1 y1 y2) → Prop).
+ P a b a b (refl ??) → P a b c d e.
+#a;#b;#c;#d;#e;#P;#HP;
+ndiscriminate e;#e0;
+nsubst e0;#e1;
+nsubst e1;#E;
+(* nsubst E; purtroppo al momento funziona solo nel verso sbagliato *)
+nrewrite > E;
+napply HP;
+nqed.*)
+
+(***************)
+
+ninductive I1 : Type[0] ≝
+| k1 : I1.
+
+ninductive I2 : I1 → Type[0] ≝
+| k2 : ∀x.I2 x.
+
+ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
+| k3 : ∀x,y.I3 x y.
+
+ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
+| k4 : ∀x,y.∀z:I3 x y.I4 x y z.
+
+(*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
+
+ndefinition R4 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (refl T0 a0).
+ ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
+ Type[0].
+ ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
+ a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ a3).
+ ∀b0:T0.
+ ∀e0:eq (T0 …) a0 b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+ ∀b3: T3 b0 e0 b1 e1 b2 e2.
+ ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+ T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+napply (eq_rect_Type0 ????? e3);
+napply (R3 ????????? e0 ? e1 ? e2);
+napply a4;
+nqed.
+
+
+ninductive II : Type[0] ≝
+| kII1 : ∀x,y,z.∀w:I4 x y z.II
+| kII2 : ∀x,y,z.∀w:I4 x y z.II.
+
+(* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
+#a;#b;#c;#d;#e;#f;#g;#h;#H;
+ndiscriminate H;
+nqed. *)
+
+nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
+ ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
+ P e f g h (refl ??) → P a b c d Heq.
+#a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
+ndestruct;
+napply HP;
+nqed.
#A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
nqed.
+nlemma eq_ind_r :
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
+nqed.
+
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
universe constraint Type[0] < Type[1].
universe constraint Type[1] < Type[2].
universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
∀b1: T1 b0 e0.
∀e1:R1 ??? a1 ? e0 = b1.
T2 b0 e0 b1 e1.
-intros 9;intro e1;
+intros (T0 a0 T1 a1 T2 a2);
apply (eq_rect' ????? e1);
apply (R1 ?? ? ?? e0);
simplify;assumption;
∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
∀x2:T2 x0 p0 x1 p1.R2 T0 a0 T1 a1 T2 a2 ? p0 ? p1 = x2→ Type.
+ ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
∀e1:R1 ??? a1 ? e0 = b1.
∀b2: T2 b0 e0 b1 e1.
∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
- ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
-intros 12;intros 2 (e2 H);
+ T3 b0 e0 b1 e1 b2 e2.
+intros (T0 a0 T1 a1 T2 a2 T3 a3);
apply (eq_rect' ????? e2);
apply (R2 ?? ? ???? e0 ? e1);
simplify;assumption;
inductive I3 : Type ≝
| kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
-definition I3d: I3 → I3 → Type ≝
-λx,y.match x with
+(* lemma idfof : (∀t1,t2,t3,u1,u2,u3.((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.
+ λy3:I2 y1 y2.λp3:R2 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 (λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1 =y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t3 y1 p1 y2 p2 =y3.
+ kI3 y1 y2 y3 =kI3 u1 u2 u3)
+t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)
+ t3 (refl_eq ((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)) t3)
+ )
+ → True).
+simplify; *)
+
+definition I3d : ∀x,y:I3.x = y → Type ≝
+λx,y.match x return (λx:I3.x = y → Type) with
+[ kI3 x1 x2 x3 ⇒ match y return (λy:I3.kI3 x1 x2 x3 = y → Type) with
+ [ kI3 y1 y2 y3 ⇒
+ λe:kI3 x1 x2 x3 = kI3 y1 y2 y3.
+ ∀P:Prop.(∀e1: x1 = y1.
+ ∀e2: R1 ?? (λz1,p1.I1 z1) ?? e1 = y2.
+ ∀e3: R2 ???? (λz1,p1,z2,p2.I2 z1 z2) x3 ? e1 ? e2 = y3.
+ R3 ??????
+ (λz1,p1,z2,p2,z3,p3.
+ eq ? (kI3 z1 z2 z3) (kI3 y1 y2 y3)) e y1 e1 y2 e2 y3 e3
+ = refl_eq ? (kI3 y1 y2 y3)
+ → P) → P]].
+
+definition I3d : ∀x,y:I3.x=y → Type.
+intros 2;cases x;cases y;intro;
+apply (∀P:Prop.(∀e1: x1 = x3.
+ ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = x4.
+ ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) i ? e1 ? e2 = i1.
+ R3 ??????
+ (λy1,p1,y2,p2,y3,p3.
+ eq ? (kI3 y1 y2 y3) (kI3 x3 x4 i1)) H x3 e1 x4 e2 i1 e3
+ = refl_eq ? (kI3 x3 x4 i1)
+ → P) → P);
+qed.
+
+(* definition I3d : ∀x,y:nat. x = y → Type ≝
+λx,y.
+match x
+ return (λx.x = y → Type)
+ with
+[ O ⇒ match y return (λy.O = y → Type) with
+ [ O ⇒ λe:O = O.∀P.P → P
+ | S q ⇒ λe: O = S q. ∀P.P]
+| S p ⇒ match y return (λy.S p = y → Type) with
+ [ O ⇒ λe:S p = O.∀P.P
+ | S q ⇒ λe: S p = S q. ∀P.(p = q → P) → P]].
+
+definition I3d:
+ ∀x,y:I3. x = y → Type
+ ≝
+λx,y.
+match x with
+[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
+ [ kI3 u1 u2 u3 ⇒ λe:kI3 t1 t2 t3 = kI3 u1 u2 u3.∀P:Type.
+ (∀e1: t1 = u1.
+ ∀e2: R1 nat t1 (λy1:nat.λp1:y1 = u1.I1 y1) t2 ? e1 = u2.
+ ∀e3: R2 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3.
+ (* ∀e: kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+ R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3
+ (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) e u1 e1 u2 e2 u3 e3 = refl_eq I3 (kI3 u1 u2 u3)
+ → P)
+ → P]].
+
+definition I3d:
+ ∀x,y:I3.
+ (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+ match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]) → Type
+ ≝
+λx,y.λe:
+ (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+ match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]).
+match x with
[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
[ kI3 u1 u2 u3 ⇒ ∀P:Type.
(∀e1: t1 = u1.
∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
- ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) ? e1 ? e2 t3 = u3.P) → P]].
-
-lemma I3nc : ∀a,b.a = b → I3d a b.
-intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
+ ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3.
+ (* ∀e: kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+ R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3
+ (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) (e (kI3 t1 t2 t3) (kI3 u1 u2 u3)) u1 e1 u2 e2 u3 e3 = refl_eq ? (kI3 u1 u2 u3)
+ → P)
+ → P]].*)
+
+lemma I3nc : ∀a,b.∀e:a = b. I3d a b e.
+intros;apply (R1 ????? e);elim a;whd;intros;apply H;reflexivity;
qed.
(*lemma R1_r : ΠA:Type.Πx:A.ΠP:Πy:A.y=x→Type.P x (refl_eq A x)→Πy:A.Πp:y=x.P y p.
simplify;assumption;
qed.*)
-definition I3prova : ∀a,b,c,d,e,f.kI3 a b c = kI3 d e f → ∃P.P d e f.
-intros;apply (I3nc ?? H);clear H;
+definition I3prova : ∀a,b,c,d,e,f.∀Heq:kI3 a b c = kI3 d e f.
+ ∀P:? → ? → ? → ? → Prop.
+ P d e f Heq →
+ P a b c (refl_eq ??).
+intros;apply (I3nc ?? Heq);
simplify;intro;
+generalize in match H as H;generalize in match Heq as Heq;
generalize in match f as f;generalize in match e as e;
-generalize in match c as c;generalize in match b as b;
-clear f e c b;
+clear H Heq f e;
apply (R1 ????? e1);intros 5;simplify in e2;
-generalize in match f as f;generalize in match c as c;
-clear f c;
-apply (R1 ????? e2);intros;simplify in H;
-elim daemon;
+generalize in match H as H;generalize in match Heq as Heq;
+generalize in match f as f;
+clear H Heq f;
+apply (R1 ????? e2);intros 4;simplify in e3;
+generalize in match H as H;generalize in match Heq as Heq;
+clear H Heq;
+apply (R1 ????? e3);intros;simplify in H1;
+apply (R1 ????? H1);
+assumption;
qed.
projects / helm.git / commitdiff