From 2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 16 Nov 2009 17:09:31 +0000 Subject: [PATCH] Implementation of ndestruct tactic (including destruction of constructor forms in the dependently typed case; not including discrimination of cycles). --- .../components/acic_content/.depend.opt | 3 - .../components/acic_procedural/.depend.opt | 7 - .../components/binaries/extractor/.depend.opt | 4 - .../binaries/table_creator/.depend.opt | 2 - .../components/binaries/transcript/.depend | 5 - .../binaries/transcript/.depend.opt | 5 - helm/software/components/cic/.depend.opt | 2 - helm/software/components/cic_acic/.depend.opt | 3 - .../components/cic_disambiguation/.depend.opt | 2 - .../components/cic_exportation/.depend.opt | 1 - .../components/cic_proof_checking/.depend.opt | 10 -- .../components/cic_unification/.depend.opt | 7 - .../components/content_pres/.depend.opt | 6 - .../components/disambiguation/.depend.opt | 1 - helm/software/components/extlib/.depend.opt | 10 -- helm/software/components/getter/.depend.opt | 7 - helm/software/components/grafite/.depend.opt | 2 - .../software/components/grafite/grafiteAst.ml | 7 +- .../components/grafite/grafiteAstPp.ml | 5 + .../components/grafite_engine/.depend.opt | 1 - .../grafite_engine/grafiteEngine.ml | 22 +++ .../components/grafite_parser/.depend.opt | 5 - .../grafite_parser/grafiteParser.ml | 5 + helm/software/components/hgdome/.depend.opt | 2 - helm/software/components/hmysql/.depend.opt | 5 - helm/software/components/lexicon/.depend.opt | 2 - helm/software/components/library/.depend.opt | 9 - helm/software/components/logger/.depend.opt | 1 - helm/software/components/metadata/.depend.opt | 2 - .../components/ng_cic_content/.depend.opt | 2 - .../components/ng_disambiguation/.depend.opt | 1 - helm/software/components/ng_kernel/.depend | 1 - .../software/components/ng_kernel/.depend.opt | 1 - .../components/ng_kernel/nCicTypeChecker.mli | 4 + helm/software/components/ng_library/.depend | 3 - .../components/ng_library/.depend.opt | 3 - .../components/ng_paramodulation/.depend.opt | 2 - .../components/ng_refiner/.depend.opt | 3 - helm/software/components/ng_tactics/.depend | 13 +- .../components/ng_tactics/.depend.opt | 13 +- helm/software/components/ng_tactics/Makefile | 3 +- .../components/ng_tactics/nTacStatus.ml | 4 + .../components/ng_tactics/nTacStatus.mli | 1 + .../components/ng_tactics/nTactics.ml | 4 +- .../components/ng_tactics/nTactics.mli | 27 +++ helm/software/components/registry/.depend.opt | 1 - .../components/syntax_extensions/.depend | 3 - .../components/syntax_extensions/.depend.opt | 3 - helm/software/components/tactics/.depend.opt | 11 -- helm/software/components/thread/.depend.opt | 2 - .../components/tptp_grafite/.depend.opt | 3 - .../components/urimanager/.depend.opt | 1 - helm/software/components/whelp/.depend.opt | 2 - helm/software/components/xml/.depend.opt | 2 - helm/software/components/xmldiff/.depend.opt | 1 - helm/software/matita/.depend | 17 -- .../software/matita/contribs/POPLmark/depends | 10 +- helm/software/matita/matita.lang | 3 +- .../matita/nlibrary/logic/destruct_bb.ma | 158 +++++++++++++----- .../matita/nlibrary/logic/equality.ma | 5 + helm/software/matita/nlibrary/logic/pts.ma | 1 + helm/software/matita/tests/destruct_bb.ma | 118 +++++++++++-- 62 files changed, 323 insertions(+), 246 deletions(-) diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt index 307fceaa0..fef879256 100644 --- a/helm/software/components/acic_content/.depend.opt +++ b/helm/software/components/acic_content/.depend.opt @@ -1,4 +1,3 @@ -content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmx @@ -6,8 +5,6 @@ cicNotationEnv.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 diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 97238c4d8..8d0128744 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,13 +1,6 @@ -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 diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt index 0c39328ae..e69de29bb 100644 --- a/helm/software/components/binaries/extractor/.depend.opt +++ b/helm/software/components/binaries/extractor/.depend.opt @@ -1,4 +0,0 @@ -extractor.cmo: -extractor.cmx: -extractor_manager.cmo: -extractor_manager.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt index 33147b949..e69de29bb 100644 --- a/helm/software/components/binaries/table_creator/.depend.opt +++ b/helm/software/components/binaries/table_creator/.depend.opt @@ -1,2 +0,0 @@ -table_creator.cmo: -table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ 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 diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ 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 diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 8cdd2a86a..76d19c1ff 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -1,10 +1,8 @@ -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 diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt index 5449d50aa..3fc1e0dce 100644 --- a/helm/software/components/cic_acic/.depend.opt +++ b/helm/software/components/cic_acic/.depend.opt @@ -1,6 +1,3 @@ -eta_fixing.cmi: -doubleTypeInference.cmi: -cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt index a9ae65a5e..e9bd1168f 100644 --- a/helm/software/components/cic_disambiguation/.depend.opt +++ b/helm/software/components/cic_disambiguation/.depend.opt @@ -1,5 +1,3 @@ -cicDisambiguate.cmi: -disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt index 91be8d88d..288ea5f6c 100644 --- a/helm/software/components/cic_exportation/.depend.opt +++ b/helm/software/components/cic_exportation/.depend.opt @@ -1,3 +1,2 @@ -cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt index f8a16629e..5d83fd0f3 100644 --- a/helm/software/components/cic_proof_checking/.depend.opt +++ b/helm/software/components/cic_proof_checking/.depend.opt @@ -1,13 +1,3 @@ -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 diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt index 2e054f73d..a7b23ceb4 100644 --- a/helm/software/components/cic_unification/.depend.opt +++ b/helm/software/components/cic_unification/.depend.opt @@ -1,10 +1,3 @@ -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 diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt index 8d74439eb..6dd0e78a1 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -1,9 +1,3 @@ -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 diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt index 9fdbeeeaf..aba9ffea7 100644 --- a/helm/software/components/disambiguation/.depend.opt +++ b/helm/software/components/disambiguation/.depend.opt @@ -1,4 +1,3 @@ -disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt index dcc6377a0..201cd0cba 100644 --- a/helm/software/components/extlib/.depend.opt +++ b/helm/software/components/extlib/.depend.opt @@ -1,13 +1,3 @@ -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 diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt index 64da37f13..554fb1ec7 100644 --- a/helm/software/components/getter/.depend.opt +++ b/helm/software/components/getter/.depend.opt @@ -1,13 +1,6 @@ -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 diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt index e01d5bbfa..0f64ba789 100644 --- a/helm/software/components/grafite/.depend.opt +++ b/helm/software/components/grafite/.depend.opt @@ -1,7 +1,5 @@ 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 diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 0cfdef148..7754102c6 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -57,6 +57,9 @@ type ntactic = | 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 @@ -71,6 +74,7 @@ type ntactic = | NBranch of loc | NShift of loc | NPos of loc * int list + | NPosbyname of loc * string | NWildcard of loc | NMerge of loc | NSkip of loc @@ -197,7 +201,7 @@ type nmacro = (** 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 *) @@ -220,6 +224,7 @@ type ('term,'obj) command = 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 83f3a36b6..0db8efc1a 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -111,6 +111,9 @@ let rec pp_ntactic ~map_unicode_to_tex = | 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" @@ -125,6 +128,7 @@ let rec pp_ntactic ~map_unicode_to_tex = | NBranch _ -> "##[" | NShift _ -> "##|" | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":" + | NPosbyname (_, s) -> "##" ^ s ^ ":" | NWildcard _ -> "##*:" | NMerge _ -> "##]" | NFocus (_,l) -> @@ -371,6 +375,7 @@ let pp_coercion ~term_pp t do_composites arity saturations= let pp_ncommand = function | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + | NDiscriminator (_,_) | NInverter (_,_,_,_,_) | NObj (_,_) | NUnivConstraint (_) -> "not supported" diff --git a/helm/software/components/grafite_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt index 10236823a..a545f14e3 100644 --- a/helm/software/components/grafite_engine/.depend.opt +++ b/helm/software/components/grafite_engine/.depend.opt @@ -1,4 +1,3 @@ -grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index fd8d776c1..248c02fa5 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -759,6 +759,9 @@ let eval_ng_tac tac = 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 @@ -775,6 +778,7 @@ let eval_ng_tac 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) -> @@ -991,6 +995,24 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = [] -> 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") diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 2766b04d0..97bf4d7c2 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -1,9 +1,4 @@ -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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 0fc42291d..2914a8906 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -257,6 +257,9 @@ EXTEND 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 -> @@ -566,6 +569,7 @@ EXTEND | 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 @@ -803,6 +807,7 @@ EXTEND 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 ] -> diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt index 072d9697a..bf9c09af7 100644 --- a/helm/software/components/hgdome/.depend.opt +++ b/helm/software/components/hgdome/.depend.opt @@ -1,5 +1,3 @@ -domMisc.cmi: -xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt index c2289bff2..602c901b8 100644 --- a/helm/software/components/hmysql/.depend.opt +++ b/helm/software/components/hmysql/.depend.opt @@ -1,7 +1,2 @@ -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 diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt index 0fee4b18e..463d8a7bc 100644 --- a/helm/software/components/lexicon/.depend.opt +++ b/helm/software/components/lexicon/.depend.opt @@ -3,8 +3,6 @@ lexiconMarshal.cmi: lexiconAst.cmx 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 diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt index cfa1295ed..a9f24f814 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -1,13 +1,4 @@ -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 diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt index dfb4400ff..28268d29e 100644 --- a/helm/software/components/logger/.depend.opt +++ b/helm/software/components/logger/.depend.opt @@ -1,3 +1,2 @@ -helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt index 78cd97a0d..492a34e3a 100644 --- a/helm/software/components/metadata/.depend.opt +++ b/helm/software/components/metadata/.depend.opt @@ -1,5 +1,3 @@ -sqlStatements.cmi: -metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt index 1316c8eab..b4e17fa99 100644 --- a/helm/software/components/ng_cic_content/.depend.opt +++ b/helm/software/components/ng_cic_content/.depend.opt @@ -1,5 +1,3 @@ -ncic2astMatcher.cmi: -nTermCicContent.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt index 2de54dc5e..6b4ef95c1 100644 --- a/helm/software/components/ng_disambiguation/.depend.opt +++ b/helm/software/components/ng_disambiguation/.depend.opt @@ -1,3 +1,2 @@ -nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 9a4ae3fc1..4d6080d8a 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,4 +1,3 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index d7c542af5..d4a4f8303 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,4 +1,3 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index 3cd11c0f8..c57055365 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -59,3 +59,7 @@ val debruijn: 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 diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend index e379b9fc6..5e568e6b3 100644 --- a/helm/software/components/ng_library/.depend +++ b/helm/software/components/ng_library/.depend @@ -1,6 +1,3 @@ -nCic2OCic.cmi: -oCic2NCic.cmi: -nCicLibrary.cmi: nCic2OCic.cmo: nCic2OCic.cmi nCic2OCic.cmx: nCic2OCic.cmi oCic2NCic.cmo: oCic2NCic.cmi diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt index e379b9fc6..5e568e6b3 100644 --- a/helm/software/components/ng_library/.depend.opt +++ b/helm/software/components/ng_library/.depend.opt @@ -1,6 +1,3 @@ -nCic2OCic.cmi: -oCic2NCic.cmi: -nCicLibrary.cmi: nCic2OCic.cmo: nCic2OCic.cmi nCic2OCic.cmx: nCic2OCic.cmi oCic2NCic.cmo: oCic2NCic.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 369ed6b69..3ace51014 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,4 +1,3 @@ -terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi @@ -11,7 +10,6 @@ paramod.cmi: terms.cmi orderings.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 diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index db7e52884..f30b906fd 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,6 +1,3 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 2e709a0af..ef100f742 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,11 +1,8 @@ -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 @@ -18,7 +15,9 @@ zipTree.cmo: zipTree.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 diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 2e709a0af..ef100f742 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,11 +1,8 @@ -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 @@ -18,7 +15,9 @@ zipTree.cmo: zipTree.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 diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index f05c75e94..6bb0ac3ee 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -8,7 +8,8 @@ INTERFACE_FILES = \ zipTree.mli \ andOrTree.mli \ nAuto.mli \ - nInversion.mli + nInversion.mli \ + nDestructTac.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index b6013c272..b58eb5558 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -229,6 +229,10 @@ let get_goalty status g = 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 diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index ec9f7738a..bf2370ec9 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -62,6 +62,7 @@ val saturate : 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 -> diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index d366c87d2..10fa168d4 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -52,7 +52,7 @@ let branch_tac status = | [] -> 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 @@ -478,6 +478,8 @@ type indtyinfo = { } ;; +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 diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index b8659c357..25baae97a 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -48,6 +48,7 @@ val rewrite_tac: 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 @@ -61,3 +62,29 @@ val assert_tac: 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 diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt index 40c03891a..cf4f36b68 100644 --- a/helm/software/components/registry/.depend.opt +++ b/helm/software/components/registry/.depend.opt @@ -1,3 +1,2 @@ -helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt index 3d7dfc21f..c0cd9c906 100644 --- a/helm/software/components/syntax_extensions/.depend.opt +++ b/helm/software/components/syntax_extensions/.depend.opt @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index d9d6034a1..169fc76b0 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -1,19 +1,11 @@ -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 @@ -35,13 +27,10 @@ equalityTactics.cmi: proofEngineTypes.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 diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt index 6616a03d0..7759190c6 100644 --- a/helm/software/components/thread/.depend.opt +++ b/helm/software/components/thread/.depend.opt @@ -1,5 +1,3 @@ -threadSafe.cmi: -extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt index fb60fe8f2..c74300207 100644 --- a/helm/software/components/tptp_grafite/.depend.opt +++ b/helm/software/components/tptp_grafite/.depend.opt @@ -1,7 +1,4 @@ parser.cmi: ast.cmx -tptp2grafite.cmi: -ast.cmo: -ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmx parser.cmi diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt index 9cac9aa78..482148423 100644 --- a/helm/software/components/urimanager/.depend.opt +++ b/helm/software/components/urimanager/.depend.opt @@ -1,3 +1,2 @@ -uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt index 65dc07955..39f37dfa9 100644 --- a/helm/software/components/whelp/.depend.opt +++ b/helm/software/components/whelp/.depend.opt @@ -1,5 +1,3 @@ -whelp.cmi: -fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt index e7e7ffbd7..5ef59bdc9 100644 --- a/helm/software/components/xml/.depend.opt +++ b/helm/software/components/xml/.depend.opt @@ -1,5 +1,3 @@ -xml.cmi: -xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt index 65bd7b949..e2832de33 100644 --- a/helm/software/components/xmldiff/.depend.opt +++ b/helm/software/components/xmldiff/.depend.opt @@ -1,3 +1,2 @@ -xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index c9a27fc56..9ebd03a64 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -1,7 +1,5 @@ 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 @@ -26,8 +24,6 @@ matitaEngine.cmo: applyTransformation.cmi matitaEngine.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 \ @@ -72,21 +68,8 @@ predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi 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: diff --git a/helm/software/matita/contribs/POPLmark/depends b/helm/software/matita/contribs/POPLmark/depends index 02154bda1..7e7b8ae97 100644 --- a/helm/software/matita/contribs/POPLmark/depends +++ b/helm/software/matita/contribs/POPLmark/depends @@ -1,10 +1,12 @@ -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 diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 6a24b9aed..8b9577181 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -206,7 +206,8 @@ nchange nrewrite ncut - nlapply + nlapply + ndestruct diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma index f188bf80f..49a03ff0f 100644 --- a/helm/software/matita/nlibrary/logic/destruct_bb.ma +++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma @@ -11,51 +11,34 @@ (* 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 : @@ -63,19 +46,112 @@ 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. diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index 715423143..b92f92f66 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -28,6 +28,11 @@ nlemma eq_rect_CProp0_r: #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)). diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma index 8a44b8300..d9db8c39f 100644 --- a/helm/software/matita/nlibrary/logic/pts.ma +++ b/helm/software/matita/nlibrary/logic/pts.ma @@ -15,3 +15,4 @@ universe constraint Type[0] < Type[1]. universe constraint Type[1] < Type[2]. universe constraint Type[2] < Type[3]. +universe constraint Type[3] < Type[4]. diff --git a/helm/software/matita/tests/destruct_bb.ma b/helm/software/matita/tests/destruct_bb.ma index 494d5805a..382620e34 100644 --- a/helm/software/matita/tests/destruct_bb.ma +++ b/helm/software/matita/tests/destruct_bb.ma @@ -79,7 +79,7 @@ definition R2 : ∀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; @@ -94,14 +94,15 @@ definition R3 : ∀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; @@ -194,16 +195,91 @@ inductive I2 : ∀n:nat.I1 n → Type ≝ 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. @@ -231,17 +307,25 @@ apply (R1_r ?? ? ?? e0); 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. -- 2.39.2