From: Wilmer Ricciotti Date: Tue, 17 Nov 2009 13:01:53 +0000 (+0000) Subject: ndestruct tactic: mainly bugfixes; the algorithm isn't clean yet, outputting a X-Git-Tag: make_still_working~3205 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b98af47f4359ca20b42e52285c7ff4a3bd12f02;p=helm.git ndestruct tactic: mainly bugfixes; the algorithm isn't clean yet, outputting a number of unnecessary equations which must be cleared; it seems to work reasonably nonetheless. --- diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml new file mode 100644 index 000000000..776d5dace --- /dev/null +++ b/helm/software/components/ng_tactics/nDestructTac.ml @@ -0,0 +1,465 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *) + +open NTacStatus + +let debug = true +let pp = + if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) + +let fresh_name = + let i = ref 0 in + function () -> + incr i; + "z" ^ string_of_int !i +;; + +let mk_id id = + let id = if id = "_" then fresh_name () else id in + CicNotationPt.Ident (id,None) +;; + +let mk_appl = + function + [] -> assert false + | [x] -> x + | l -> CicNotationPt.Appl l +;; + +let rec iter f n acc = + if n < 0 then acc + else iter f (n-1) (f n acc) +;; + +let subst_metasenv_and_fix_names status = + let u,h,metasenv, subst,o = status#obj in + let o = + NCicUntrusted.map_obj_kind ~skip_body:true + (NCicUntrusted.apply_subst subst []) o + in + status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) +;; + +(* input: nome della variabile riscritta + * output: lista dei nomi delle variabili il cui tipo dipende dall'input *) +let cascade_select_in_ctx ~subst ctx iname = + prerr_endline "C"; + let lctx, rctx = HExtlib.split_nth (iname - 1) ctx in + let lctx = List.rev lctx in + let rec rm_last = function + [] | [_] -> [] + | hd::tl -> hd::(rm_last tl) + in + + let indices,_ = List.fold_left + (fun (acc,context) item -> + prerr_endline "C2"; + match item with + | n,(NCic.Decl s | NCic.Def (s,_)) + when not (List.for_all (fun x -> NCicTypeChecker.does_not_occur ~subst context (x-1) x s) acc) -> + List.iter (fun m -> prerr_endline ("acc has " ^ (string_of_int m))) acc; + prerr_endline ("acc occurs in the type of " ^ n); + (1::List.map ((+) 1) acc, item::context) + | _ -> (List.map ((+) 1) acc, item::context)) + ([1], rctx) lctx in + prerr_endline "C3:"; + List.iter (fun n -> prerr_endline (string_of_int n)) indices; + let indices = match rm_last indices with + | [] -> [] + | _::tl -> tl in + let res = List.map (fun n -> let s,_ = List.nth ctx (n-1) in s) indices in + prerr_endline "C4:"; + List.iter (fun n -> prerr_endline n) res; + prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst ctx); + res, indices +;; + +let rec mk_fresh_name ctx firstch n = + let candidate = (String.make 1 firstch) ^ (string_of_int n) in + if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate + else mk_fresh_name ctx firstch (n+1) +;; + +let arg_list nleft t = + let rec drop_prods n t = + if n <= 0 then t + else match t with + | NCic.Prod (_,_,ta) -> drop_prods (n-1) ta + | _ -> raise (Failure "drop_prods") + in + let rec aux = function + | NCic.Prod (_,so,ta) -> so::aux ta + | _ -> [] + in aux (drop_prods nleft t) +;; + +let nargs it nleft consno = + prerr_endline (Printf.sprintf "nargs %d %d" nleft consno); + let _,indname,_,cl = it in + let _,_,t_k = List.nth cl consno in + List.length (arg_list nleft t_k) ;; + +let default_pattern = "",0,(None,[],Some CicNotationPt.UserInput);; + +(* returns the discrimination = injection+contradiction principle *) +(* FIXME: mi riservo di considerare tipi con parametri sx alla fine *) + +let mk_discriminator it status = + let nleft = 0 in + let _,indname,_,cl = it in + + + let mk_eq tys ts us es n = + (* eqty = Tn u0 e0...un-1 en-1 *) + let eqty = mk_appl + (List.nth tys n :: iter (fun i acc -> + List.nth us i:: + List.nth es i:: acc) + (n-1) []) in + + (* params = [T0;t0;...;Tn;tn;u0;e0;un-1;en-1] *) + let params = iter (fun i acc -> + List.nth tys i :: + List.nth ts i :: acc) n + (iter (fun i acc -> + List.nth us i:: + List.nth es i:: acc) (n-1) []) in + mk_appl [mk_id "eq"; eqty; + mk_appl (mk_id ("R" ^ string_of_int n) :: params); + List.nth us n] + in + + let kname it j = + let _,_,_,cl = it in + let _,name,_ = List.nth cl j in + name + in + + let branch i j ts us = + let nargs = nargs it nleft i in + let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in + let tys = List.map + (fun x -> CicNotationPt.Implicit (`Tagged ("T" ^ (string_of_int x)))) + (HExtlib.list_seq 0 nargs) in + let tys = tys @ + [iter (fun i acc -> + CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), + CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), + acc))) (nargs-1) + (mk_appl [mk_id "eq"; CicNotationPt.Implicit `JustOne; + mk_appl (mk_id (kname it i):: + List.map (fun x -> mk_id ("x" ^string_of_int x)) + (HExtlib.list_seq 0 (List.length ts))); + mk_appl (mk_id (kname it j)::us)])] + in + CicNotationPt.Binder (`Lambda, (mk_id "e", + Some (mk_appl + [mk_id "eq"; + CicNotationPt.Implicit `JustOne; + mk_appl (mk_id (kname it i)::ts); + mk_appl (mk_id (kname it j)::us)])), + let ts = ts @ [mk_id "e"] in + let refl2 = mk_appl + [mk_id "refl"; + CicNotationPt.Implicit `JustOne; + mk_appl (mk_id (kname it j)::us)] in + let us = us @ [refl2] in + CicNotationPt.Binder (`Forall, (mk_id "P", Some (CicNotationPt.Sort (`NType "1") )), + if i = j then + CicNotationPt.Binder (`Forall, (mk_id "_", + Some (iter (fun i acc -> + CicNotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc)) + (nargs-1) + (CicNotationPt.Binder (`Forall, (mk_id "_", + Some (mk_eq tys ts us es nargs)), + mk_id "P")))), mk_id "P") + else mk_id "P")) + in + + let inner i ts = CicNotationPt.Case + (mk_id "y",None, + Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None), + CicNotationPt.Binder (`Forall, (mk_id "_", Some + (mk_appl [mk_id "eq";CicNotationPt.Implicit + `JustOne;CicNotationPt.Implicit `JustOne;mk_id "y"])), + CicNotationPt.Implicit `JustOne ))), + List.map + (fun j -> + let nargs_kty = nargs it nleft j in + let us = iter (fun m acc -> mk_id ("u" ^ (string_of_int m))::acc) + (nargs_kty - 1) [] in + let nones = + iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in + CicNotationPt.Pattern (kname it j, + None, + List.combine us nones), + branch i j ts us) + (HExtlib.list_seq 0 (List.length cl))) + in + let outer = CicNotationPt.Case + (mk_id "x",None, + Some (CicNotationPt.Binder (`Lambda, (mk_id "_",None), + (*CicNotationPt.Sort (`NType "2")*) CicNotationPt.Implicit + `JustOne)) , + List.map + (fun i -> + let nargs_kty = nargs it nleft i in + let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc) + (nargs_kty - 1) [] in + let nones = + iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in + CicNotationPt.Pattern (kname it i, + None, + List.combine ts nones), + inner i ts) + (HExtlib.list_seq 0 (List.length cl))) in + let principle = CicNotationPt.Binder (`Lambda, (mk_id "x", Some (mk_id indname)), + CicNotationPt.Binder (`Lambda, (mk_id "y", Some (mk_id indname)), outer)) + in + pp (lazy ("discriminator = " ^ (CicNotationPp.pp_term principle))); + + status, principle +;; + +let hd_of_term = function + | NCic.Appl (hd::_) -> hd + | t -> t +;; + +let name_of_rel ~context rel = + let s, _ = List.nth context (rel-1) in s +;; + +(* let lookup_in_ctx ~context n = + List.nth context ((List.length context) - n - 1) +;;*) + +let discriminate_tac ~context cur_eq status = + pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); + + let dbranch it leftno consno = + prerr_endline (Printf.sprintf "dbranch %d %d" leftno consno); + let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in + (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *) + let params = List.map (fun x -> prerr_endline (Printf.sprintf "dbranch param a%d" x); NTactics.intro_tac ("a" ^ string_of_int x)) nlist in + NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern:: + params @ [ + NTactics.intro_tac "P"; + NTactics.intro_tac "DH"; + NTactics.apply_tac ("",0,mk_id "DH"); + NTactics.apply_tac ("",0,mk_id "refl"); + ] in + let dbranches it leftno = + prerr_endline (Printf.sprintf "dbranches %d" leftno); + let _,_,_,cl = it in + let nbranches = List.length cl in + let branches = iter (fun n acc -> + let m = nbranches - n - 1 in + if m = 0 then (prerr_endline "no shift"; acc @ (dbranch it leftno m)) + else (prerr_endline "sì shift"; acc @ NTactics.shift_tac :: (dbranch it + leftno m))) + (nbranches-1) [] in + if nbranches > 1 then + (prerr_endline "sì branch"; + NTactics.branch_tac:: branches @ [NTactics.merge_tac]) + else + (prerr_endline "no branch"; + branches) + in + + let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in + let _,ctx' = HExtlib.split_nth cur_eq context in + let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in + let status, s = term_of_cic_term status s ctx' in + let status, leftno, it = + let it, t1, t2 = match s with + | NCic.Appl [_;it;t1;t2] -> it,t1,t2 + | _ -> assert false in + (* XXX: serve? ho già fatto whd *) + let status, it = whd status ctx' (mk_cic_term ctx' it) in + let status, it = term_of_cic_term status it ctx' in + let _uri,indtyno,its = match it with + NCic.Const (NReference.Ref (uri, NReference.Ind (_,indtyno,_)) as r) -> + uri, indtyno, NCicEnvironment.get_checked_indtys r + | _ -> prerr_endline ("discriminate: indty =" ^ NCicPp.ppterm + ~metasenv:[] ~subst:[] ~context:[] it) ; assert false in + let _,leftno,its,_,_ = its in + status, leftno, List.nth its indtyno + in + + NTactics.block_tac ( + [(fun status -> + let status, discr = mk_discriminator it status in + NTactics.cut_tac ("",0, CicNotationPt.Binder (`Forall, (mk_id "x", None), + CicNotationPt.Binder (`Forall, (mk_id "y", None), + CicNotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl [mk_id "eq";CicNotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), + mk_appl [discr; mk_id "x"; mk_id "y"; + mk_id "e"])))) + status); + NTactics.branch_tac; + NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; + NTactics.intro_tac "x"; + NTactics.intro_tac "y"; + NTactics.intro_tac "Deq"; + NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; + NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] + @ dbranches it leftno @ + [NTactics.shift_tac; + NTactics.intro_tac "discriminate"; + NTactics.apply_tac ("",0,mk_appl [mk_id "discriminate"; + CicNotationPt.Implicit `JustOne; + CicNotationPt.Implicit `JustOne; mk_id eq_name ]); + NTactics.reduce_tac ~reduction:(`Normalize true) + ~where:default_pattern; + NTactics.clear_tac ["discriminate"]; + NTactics.merge_tac] + ) status +;; + +let subst_tac ~context ~dir cur_eq = + fun status -> + let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in + let _,ctx' = HExtlib.split_nth cur_eq context in + let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in + let status, s = term_of_cic_term status s ctx' in + pp (lazy (Printf.sprintf "subst: equation %s" eq_name)); + let l, r = match s with + | NCic.Appl [_;_;t1;t2] -> t1,t2 + | _ -> assert false in + let var = match dir with + | `LeftToRight -> l + | `RightToLeft -> r in + let var = match var with + | NCic.Rel i -> i + | _ -> assert false in + let names_to_gen, indices_to_gen = + cascade_select_in_ctx ~subst:(get_subst status) context (var+cur_eq) in + let moved_indices = List.fold_left + (fun acc x -> if x > cur_eq then acc+1 else acc) 0 indices_to_gen in + let gen_tac x = + NTactics.generalize_tac + ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in + NTactics.block_tac ((List.map gen_tac names_to_gen)@ + [NTactics.clear_tac names_to_gen; + NTactics.rewrite_tac ~dir + ~what:("",0,mk_id eq_name) ~where:default_pattern; + NTactics.reduce_tac ~reduction:(`Normalize true) + ~where:default_pattern]@ + (List.map NTactics.intro_tac (List.rev names_to_gen))) status, + (List.length context - cur_eq + 1 - moved_indices) +;; + +let get_ctx status = + let ref_ctx = ref [] in + let status = NTactics.distribute_tac + (fun st goal -> + let ctx = ctx_of (get_goalty st goal) in + ref_ctx := ctx; st) status in + !ref_ctx +;; + +let rec select_eq ctx i status acc = + try + match (List.nth ctx (List.length ctx - i - 1)) with + | n, (NCic.Decl s | NCic.Def (s,_)) -> + (let _,ctx_s = HExtlib.split_nth (List.length ctx - i) ctx in + let status, s = NTacStatus.whd status ctx_s (mk_cic_term ctx_s s) in + let status, s = term_of_cic_term status s ctx_s in + pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_s ~subst:[] ~metasenv:[] s))); + if (List.for_all (fun x -> x <> n) acc) then + match s with + | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;_;_] -> + if NUri.name_of_uri u = "eq" then status, Some (List.length ctx - i) + else select_eq ctx (i+1) status acc + | _ -> select_eq ctx (i+1) status acc + else select_eq ctx (i+1) status acc) + with Failure _ | Invalid_argument _ -> status, None +;; + +let classify ~subst ctx i status = + let _, (NCic.Decl s | NCic.Def (s,_)) = List.nth ctx (i-1) in + let _,ctx' = HExtlib.split_nth i ctx in + let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in + let status, s = term_of_cic_term status s ctx' in + match s with + | NCic.Appl [_;_;l;r] -> + (* FIXME: metasenv *) + if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r + then status, `Identity + else status, (match hd_of_term l, hd_of_term r with + | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref), + NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) -> + if ki != kj then `Discriminate (0,true) + else + let rit = NReference.mk_indty true kref in + let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in + let it = List.nth its itno in + let newprods = (nargs it nleft (ki-1)) + 1 in + `Discriminate (newprods, false) + | NCic.Rel j, _ + when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r -> + `Subst `LeftToRight + | _, NCic.Rel j + when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l -> + `Subst `RightToLeft + | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle + | _ -> `Blob) + | _ -> raise (Failure "classify") +;; + +let rec destruct_tac0 nprods i status acc = + let ctx = get_ctx status in + let subst = get_subst status in + let status, selection = select_eq ctx i status acc in + match selection with + | None -> + pp (lazy (Printf.sprintf "destruct: nprods is %d, i is %d, no selection, context is %s" nprods i (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + if nprods > 0 then + let status' = NTactics.intro_tac (mk_fresh_name ctx 'e' 0) status in + destruct_tac0 (nprods-1) (List.length ctx) status' acc + else + status + | Some cur_eq -> pp (lazy (Printf.sprintf + "destruct: nprods is %d, i is %d, selection is %s, context is %s" + nprods i (name_of_rel ~context:ctx cur_eq) (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + match classify ~subst ctx cur_eq status with + | status,`Discriminate (newprods,conflict) -> + let status' = discriminate_tac ~context:ctx cur_eq status in + if conflict then status' + else destruct_tac0 (nprods+newprods) (List.length ctx - cur_eq + 1) + status' (name_of_rel ~context:ctx cur_eq::acc) + | status, `Subst dir -> + let status', next_i = subst_tac ~context:ctx ~dir cur_eq status in + destruct_tac0 nprods next_i status' acc + | status, `Identity + | status, `Cycle (* TODO *) + | status, `Blob -> + destruct_tac0 nprods (cur_eq+1) status acc +;; + +let destruct_tac status = destruct_tac0 0 0 status [];; diff --git a/helm/software/components/ng_tactics/nDestructTac.mli b/helm/software/components/ng_tactics/nDestructTac.mli new file mode 100644 index 000000000..a51886511 --- /dev/null +++ b/helm/software/components/ng_tactics/nDestructTac.mli @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val destruct_tac : 's NTacStatus.tactic diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma index 49a03ff0f..c64b65118 100644 --- a/helm/software/matita/nlibrary/logic/destruct_bb.ma +++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma @@ -19,75 +19,6 @@ include "logic/equality.ma". #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 ?? 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 ?? 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 a2; -nqed. - -ndefinition R3 : - ∀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 ?? 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 ?? 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 ?? T1 a1 ? e0 = b1. - ∀b2: T2 b0 e0 b1 e1. - ∀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 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. @@ -103,42 +34,6 @@ ninductive I4 : ∀x,y.I3 x y → Type[0] ≝ (*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. @@ -154,4 +49,4 @@ nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h. #a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP; ndestruct; napply HP; -nqed. +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index b92f92f66..6fdac61b9 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -37,10 +37,90 @@ 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)). +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 ?? 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 ?? 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 a2; +nqed. + +ndefinition R3 : + ∀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 ?? 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 ?? 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 ?? T1 a1 ? e0 = b1. + ∀b2: T2 b0 e0 b1 e1. + ∀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 a3; +nqed. + +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. + ndefinition EQ: ∀A:Type[0]. equivalence_relation A. #A; napply mk_equivalence_relation [ napply eq | napply refl | #x; #y; #H; nrewrite < H; napply refl | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption] -nqed. +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/nat/nat.ma b/helm/software/matita/nlibrary/nat/nat.ma index e9d32973b..eed1efd1c 100644 --- a/helm/software/matita/nlibrary/nat/nat.ma +++ b/helm/software/matita/nlibrary/nat/nat.ma @@ -14,7 +14,6 @@ include "hints_declaration.ma". include "logic/equality.ma". -include "sets/setoids.ma". ninductive nat: Type[0] ≝ O: nat