1. nInversion/nDestruct ported to work with jmeq properly

2. axiom streicherK in logic.ma replaced with a computational proof
3. library changed accordingly

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index 722e36740a8a570a7248e9e75e54803d2f12cde2..1df1bdf05162d844629fc3b437656cf2072b687c 100644 (file)
--- 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 cf4711db51f25320bcd6664822399e307f0b8662..397a443dbcf37a4a6970e618b6b95ffd888b9576 100644 (file)
--- 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 23ad46494dbc1f92b6b03a781174f00af168eb34..cb42b56912118374391671152644550aba10eef3 100644 (file)
--- 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 adbfd9cab304d0455ac9626ed3203602384b2734..ce857937c6b5e766e9939a3a16008e373ea8d050 100644 (file)
--- 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 9f2d758c158bf3810ca85ab8cb5bc8bf04a37036..a520ca96ff8964d0c38c7efb26b97c77605b0ace 100644 (file)
--- 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 261cd77a84ab7770205ef49756dd6ce7f91754e9..b090a8de8fc80136a2b6523ce8cc6b6cad09dd30 100644 (file)
--- 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.