From 8ea6d456f9e71babcf5adb2caee6ddd2b95047fb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Oct 2011 13:52:59 +0000 Subject: [PATCH] 1. nInversion/nDestruct ported to work with jmeq properly 2. axiom streicherK in logic.ma replaced with a computational proof 3. library changed accordingly --- matita/components/ng_tactics/nDestructTac.ml | 16 ++++-- matita/components/ng_tactics/nInversion.ml | 60 +++++++++++++++----- matita/components/ng_tactics/nnAuto.ml | 2 +- matita/matita/lib/basics/bool.ma | 5 +- matita/matita/lib/basics/jmeq.ma | 30 +++++++++- matita/matita/lib/basics/logic.ma | 14 ++++- 6 files changed, 100 insertions(+), 27 deletions(-) diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index 722e36740..1df1bdf05 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -268,11 +268,13 @@ let name_of_rel ~context rel = List.nth context ((List.length context) - n - 1) ;;*) +let mk_sym s = NotationPt.Symbol (s,0);; + let discriminate_tac ~context cur_eq status = pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); let dbranch it ~use_jmeq leftno consno = - let refl_id = mk_id (if use_jmeq then "jmrefl" else "refl") in + let refl_id = mk_sym "refl" in pp (lazy (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) *) @@ -335,9 +337,15 @@ let discriminate_tac ~context cur_eq status = let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", Some xyty), NotationPt.Binder (`Forall, (mk_id "y", Some xyty), - NotationPt.Binder (`Forall, (mk_id "e", - Some (mk_appl [mk_id "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), - mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in + (if use_jmeq then fun tgt -> + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl + [mk_sym "jmsimeq"; NotationPt.Implicit `JustOne; mk_id "x"; + NotationPt.Implicit `JustOne; mk_id "y"])),tgt) + else fun tgt -> + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl [mk_sym "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),tgt)) + (mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term status cut_term)) status in NTactics.cut_tac ("",0, cut_term) status); diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index cf4711db5..397a443db 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -26,6 +26,8 @@ let mk_id id = NotationPt.Ident (id,None) ;; +let mk_sym s = NotationPt.Symbol (s,0);; + let rec split_arity status ~subst context te = match NCicReduction.whd status ~subst context te with | NCic.Prod (name,so,ta) -> @@ -46,13 +48,41 @@ let rec mk_prods l t = | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; -let rec mk_arrows ?(pattern=false) xs ys selection target = +let rec leibpatt = function + | [] -> NotationPt.UserInput + | false::sel -> leibpatt sel + | true::sel -> NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.UserInput])), + leibpatt sel);; +let rec jmeqpatt = function + | [] -> NotationPt.UserInput + | false::sel -> jmeqpatt sel + | true::sel -> NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.UserInput + ;NotationPt.UserInput])), + jmeqpatt sel);; + +let rec mk_arrows ~jmeq xs ys selection target = match selection,xs,ys with [],[],[] -> target - | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target - | true :: l,x::xs,y::ys -> - NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])), - mk_arrows ~pattern xs ys l target) + | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target + | true :: l,x::xs,y::ys when jmeq -> + NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [mk_sym "jmsimeq" ; + NotationPt.Implicit `JustOne;x; + NotationPt.Implicit `JustOne;y])), + mk_arrows ~jmeq xs ys l target) + | true :: l,x::xs,y::ys -> + NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [mk_sym "eq" ; + NotationPt.Implicit `JustOne;x;y])), + mk_arrows ~jmeq xs ys l target) | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; @@ -65,7 +95,7 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o) ;; -let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri = +let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri = pp (lazy ("leftno = " ^ string_of_int leftno)); let _,ind_name,ty,cl = it in pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty)); @@ -105,7 +135,7 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) None -> HExtlib.mk_list true (List.length ys) | Some s -> s in - let prods = mk_arrows id_rs id_ys selection pred in + let prods = mk_arrows ~jmeq id_rs id_ys selection pred in let hyplist = let rec hypaux k = function @@ -136,7 +166,7 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) let cut_theorem = let rs = List.map (fun x -> mk_id x) rs in - mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in + mk_arrows ~jmeq rs rs selection (mk_appl (mk_id "P"::rs)) in let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), @@ -145,11 +175,8 @@ NotationPt.Implicit (`Tagged "end")); let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in let where = "",0,(None,[], - Some ( - mk_arrows ~pattern:true - (HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length ys)) - (HExtlib.mk_list NotationPt.UserInput (List.length ys)) - selection NotationPt.UserInput)) in + Some (if jmeq then jmeqpatt selection + else leibpatt selection)) in let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in let status = NTactics.block_tac @@ -160,7 +187,7 @@ NotationPt.Implicit (`Tagged "end")); NTactics.branch_tac; NTactics.case_tac "end"; NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl"); + NTactics.apply_tac ("",0,mk_sym "refl"); NTactics.shift_tac; elim_tac ~what:("",0,mk_id "Hterm") ~where; NTactics.branch_tac ~force:true] @ @@ -174,3 +201,8 @@ NotationPt.Implicit (`Tagged "end")); status,status#obj ;; +let mk_inverter name is_ind it leftno ?selection outsort status baseuri = + try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri + with NTacStatus.Error _ -> + mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri +;; diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 23ad46494..cb42b5691 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -1668,7 +1668,7 @@ auto_main flags signature cache depth status: unit = NCicParamod.is_equation status metasenv subst ctx ty in (* if the goal is an equality we artificially raise its depth up to flags.maxdepth - 1 *) - if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then + if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then (* for efficiency reasons, in this case we severely cripple the search depth *) (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1))); diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma index adbfd9cab..ce857937c 100644 --- a/matita/matita/lib/basics/bool.ma +++ b/matita/matita/lib/basics/bool.ma @@ -16,10 +16,9 @@ inductive bool: Type[0] ≝ | true : bool | false : bool. -(* destruct does not work *) theorem not_eq_true_false : true ≠ false. -@nmk #Heq change with match true with [true ⇒ False|false ⇒ True] ->Heq // qed. +@nmk #Heq destruct +qed. definition notb : bool → bool ≝ λ b:bool. match b with [true ⇒ false|false ⇒ true ]. diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma index 9f2d758c1..a520ca96f 100644 --- a/matita/matita/lib/basics/jmeq.ma +++ b/matita/matita/lib/basics/jmeq.ma @@ -23,7 +23,18 @@ definition p2: ∀S:Sigma. p1 S. qed. inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝ -jmrefl : jmeq A x A x. +refl_jmeq : jmeq A x A x. + +notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" + non associative with precedence 45 +for @{ 'jmsimeq $t $a $u $b }. + +notation > "hvbox(n break ≃ m)" + non associative with precedence 45 +for @{ 'jmsimeq ? $n ? $m }. + +interpretation "john major's equality" 'jmsimeq t x u y = (jmeq t x u y). +interpretation "john major's reflexivity" 'refl = refl_jmeq. definition eqProp ≝ λA:Prop.eq A. @@ -79,7 +90,7 @@ definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0]. qed. lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. - PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h. + PP ? (P x) (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h. #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E) lapply (G ?? (curry ?? P) ?? F) [ normalize // @@ -87,4 +98,17 @@ lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. qed. lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. - P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E. + P x (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E. + +lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. + #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % +qed. + +coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?. + +lemma eq_to_jmeq: + ∀A: Type[0]. + ∀x, y: A. + x = y → x ≃ y. + // +qed. diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 261cd77a8..b090a8de8 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -18,6 +18,7 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝ refl: eq A x x. interpretation "leibnitz's equality" 'eq t x y = (eq t x y). +interpretation "leibniz reflexivity" 'refl = refl. lemma eq_rect_r: ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. @@ -227,5 +228,14 @@ definition R4 : @a4 qed. -(* TODO concrete definition by means of proof irrelevance *) -axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. +definition eqProp ≝ λA:Prop.eq A. + +(* Example to avoid indexing and the consequential creation of ill typed + terms during paramodulation *) +example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x). +#A #x #h @(refl ? h: eqProp ? ? ?). +qed. + +theorem streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. + #T #t #P #H #p >(lemmaK ?? p) @H +qed. -- 2.39.2