new case implementation

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index de68ca0538a0de0a4a8cecea1c96b394efdc99cc..07723ea9fe9483fd18afda332169373a7a8f6666 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -652,121 +652,116 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,proofbo,proofty, attrs) = proof in
-   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-    let termty = CicReduction.whd context termty in
-    let (termty,metasenv',arguments,fresh_meta) =
-     TermUtil.saturate_term
-      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
-    let term = if arguments = [] then term else Cic.Appl (term::arguments) in
-    let uri,exp_named_subst,typeno,args =
-     match termty with
-        C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
-      | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
-          (uri,exp_named_subst,typeno,args)
-      | _ -> raise NotAnInductiveTypeToEliminate
-    in
-     let paramsno,itty,patterns =
-      match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
-         C.InductiveDefinition (tys,_,paramsno,_),_ ->
-          let _,_,itty,cl = List.nth tys typeno in
-          let rec aux n context t =
-           match n,CicReduction.whd context t with
-              0,C.Prod (name,source,target) ->
-               let fresh_name =
-                mk_fresh_name_callback metasenv' context name
-                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
-                 ~typ:source
-               in
-                C.Lambda (fresh_name,C.Implicit None,
-                 aux 0 (Some (fresh_name,C.Decl source)::context) target)
-            | n,C.Prod (name,source,target) ->
-               let fresh_name =
-                mk_fresh_name_callback metasenv' context name
-                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
-                 ~typ:source
-               in
-                aux (n-1) (Some (fresh_name,C.Decl source)::context) target
-            | 0,_ -> C.Implicit None
-            | _,_ -> assert false
-          in
-           paramsno,itty,
-           List.map (function (_,cty) -> aux paramsno context cty) cl 
-       | _ -> assert false
-     in
-     let _,right_args = 
-       List.fold_right 
-         (fun x (n,acc) -> if n > 0 then (n-1,x::acc) else (n,acc)) 
-         args (List.length args - paramsno, [])
-     in
-      let outtype =
-       let n_lambdas = List.length right_args + 1 in
-       let lifted_ty = CicSubstitution.lift n_lambdas ty in
-       let replace = ProofEngineReduction.replace_lifting
-          ~equality:(ProofEngineReduction.alpha_equivalence)
-       in
-       let captured_ty = 
-         let what = 
-           List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
-         in
-         let with_what = 
-           let rec mkargs = function 
-             | 0 -> []
-             | 1 -> [Cic.Rel 1]
-             | n -> (Cic.Implicit None)::(mkargs (n-1)) 
-           in
-           mkargs n_lambdas 
-         in
-         replace ~what ~with_what ~where:lifted_ty
+  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let termty = CicReduction.whd context termty in
+  let (termty,metasenv',arguments,fresh_meta) =
+   TermUtil.saturate_term
+    (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+  let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+  let uri,exp_named_subst,typeno,args =
+    match termty with
+    | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+    | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+        (uri,exp_named_subst,typeno,args)
+    | _ -> raise NotAnInductiveTypeToEliminate
+  in
+  let paramsno,itty,patterns,right_args =
+    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    | C.InductiveDefinition (tys,_,paramsno,_),_ ->
+       let _,left_parameters,right_args = 
+         List.fold_right 
+           (fun x (n,acc1,acc2) -> 
+             if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2)) 
+           args (List.length args - paramsno, [],[])
        in
-       let captured_term_ty = 
-         let term_ty = CicSubstitution.lift (n_lambdas-1) termty in
-         let rec mkrels = function 0 -> []|n -> (Cic.Rel n)::(mkrels (n-1)) in
-         let rec fstn acc l n = 
-           if n = 0 then acc else fstn (acc@[List.hd l]) (List.tl l) (n-1) 
-         in
-         match term_ty with
-         | C.MutInd _ -> term_ty
-         | C.Appl ((C.MutInd (a,b,c))::args) -> 
-              C.Appl ((C.MutInd (a,b,c))::
-                  fstn [] args paramsno @ mkrels (n_lambdas -1))
-         | _ -> raise NotAnInductiveTypeToEliminate
+       let _,_,itty,cl = List.nth tys typeno in
+       let rec aux left_parameters context t =
+         match left_parameters,CicReduction.whd context t with
+         | [],C.Prod (name,source,target) ->
+            let fresh_name =
+              mk_fresh_name_callback metasenv' context name ~typ:source
+            in
+             C.Lambda (fresh_name,C.Implicit None,
+             aux [] (Some (fresh_name,C.Decl source)::context) target)
+         | hd::tl,C.Prod (name,source,target) ->
+             (* left parameters instantiation *)
+             aux tl context (CicSubstitution.subst hd target)
+         | [],_ -> C.Implicit None
+         | _ -> assert false
        in
-        let rec add_lambdas = function
-          | 0 -> captured_ty
-          | 1 -> 
-              C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
-          | n -> 
-              C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
-                        C.Implicit None, (add_lambdas (n-1)))
-        in
-         add_lambdas n_lambdas
+        paramsno,itty,
+        List.map (function (_,cty) -> aux left_parameters context cty) cl,
+        right_args
+    | _ -> assert false
+  in
+  let outtype =
+    let n_right_args = List.length right_args in
+    let n_lambdas = n_right_args + 1 in
+    let lifted_ty = CicSubstitution.lift n_lambdas ty in
+    let replace = ProofEngineReduction.replace_lifting
+       ~equality:(ProofEngineReduction.alpha_equivalence)
+    in
+    let captured_ty = 
+      let what = 
+        List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
       in
-       let term_to_refine =
-        C.MutCase (uri,typeno,outtype,term,patterns)
-       in
-        let refined_term,_,metasenv'',_ = 
-         CicRefine.type_of_aux' metasenv' context term_to_refine
-           CicUniv.empty_ugraph
+      let with_what = 
+        let rec mkargs = function 
+          | 0 -> []
+          | 1 -> [Cic.Rel 1]
+          | n -> (Cic.Implicit None)::(mkargs (n-1)) 
         in
-         let new_goals =
-          ProofEngineHelpers.compare_metasenvs
-           ~oldmetasenv:metasenv ~newmetasenv:metasenv''
-         in
-         let proof' = curi,metasenv'',proofbo,proofty, attrs in
-          let proof'', new_goals' =
-           apply_tactic (apply_tac ~term:refined_term) (proof',goal)
-          in
-           (* The apply_tactic can have closed some of the new_goals *)
-           let patched_new_goals =
-            let (_,metasenv''',_,_,_) = proof'' in
-             List.filter
-              (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
-              ) new_goals @ new_goals'
-           in
-            proof'', patched_new_goals
- in
+        mkargs n_lambdas 
+      in
+      replace ~what ~with_what ~where:lifted_ty
+    in
+    let captured_term_ty = 
+      let term_ty = CicSubstitution.lift n_right_args termty in
+      let rec mkrels = function 0 -> []|n -> (Cic.Rel n)::(mkrels (n-1)) in
+      let rec fstn acc l n = 
+        if n = 0 then acc else fstn (acc@[List.hd l]) (List.tl l) (n-1) 
+      in
+      match term_ty with
+      | C.MutInd _ -> term_ty
+      | C.Appl ((C.MutInd (a,b,c))::args) -> 
+           C.Appl ((C.MutInd (a,b,c))::
+               fstn [] args paramsno @ mkrels n_right_args)
+      | _ -> raise NotAnInductiveTypeToEliminate
+    in
+    let rec add_lambdas = function
+      | 0 -> captured_ty
+      | 1 -> 
+          C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+      | n -> 
+           C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
+                     C.Implicit None, (add_lambdas (n-1)))
+    in
+    add_lambdas n_lambdas
+  in
+  let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+  let refined_term,_,metasenv'',_ = 
+    CicRefine.type_of_aux' metasenv' context term_to_refine
+      CicUniv.empty_ugraph
+  in
+  let new_goals =
+    ProofEngineHelpers.compare_metasenvs
+      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+  in
+  let proof' = curi,metasenv'',proofbo,proofty, attrs in
+  let proof'', new_goals' =
+    apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+  in
+  (* The apply_tactic can have closed some of the new_goals *)
+  let patched_new_goals =
+    let (_,metasenv''',_,_,_) = proof'' in
+      List.filter
+        (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+        new_goals @ new_goals'
+    in
+    proof'', patched_new_goals
+  in
   mk_tactic (cases_tac ~term)
 ;;
 

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index e589a33d047e65a16aa02e5a47469ecd193fe022..0f3bda302d116a7b8bfbf7a9a1736c9cfab70d23 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -62,19 +62,19 @@ definition relation_class_of_argument_class : Argument_Class → Relation_Class.
 qed.
 
 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros (X x); cases x; clear x; [2,4:clear x1] clear X; assumption.
+ intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
 qed.
 
 definition relation_of_relation_class:
  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
 qed.
 
 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  ∀R.
   carrier_of_relation_class ? (relation_class_of_argument_class R) =
    carrier_of_relation_class ? R.
- intro; cases R; reflexivity.
+intro; cases R; reflexivity.
 qed.
 
 inductive nelistT (A : Type) : Type :=
@@ -530,7 +530,7 @@ qed.
 
 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
  intros (dir R);
- cases (variance_of_argument_class R);
+ cases (variance_of_argument_class R) (a);
   [ exact dir
   | cases a;
      [ exact dir                      (* covariant *)
@@ -569,12 +569,12 @@ definition relation_of_product_of_arguments:
   | intros;
     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    cases p;
-    cases p1;
+    cases p (c p2);
+    cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
-    | exact (R b b1)
+      (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+    | exact (R p2 p3)
     ]
   ]
 qed. 

diff --git a/helm/software/matita/tests/pirrel.ma b/helm/software/matita/tests/pirrel.ma
index e9ff7ca5939fdc53e7c5115aaddab0ee96aa9679..15c1a982f388a36cf78c9983f16b85f85341d2b5 100644 (file)
--- a/helm/software/matita/tests/pirrel.ma
+++ b/helm/software/matita/tests/pirrel.ma
@@ -19,10 +19,41 @@ include "logic/equality.ma".
 
 axiom T : Type.
 
-lemma step : ∀a:T.∀H:a=a. eq_ind T a (λx.a = x) H a (sym_eq ? ? ? H) = refl_eq T a.
-intros (a H). cases H. reflexivity.
+definition step ≝ λa,b,c:T.λH1:a=b.λH2:a=c. eq_ind T ? (λx.b = x) H1 ? H2.
+
+lemma stepH : ∀a:T.∀H:a=a. step ? ? ? H H = refl_eq T a.
+intros (a H); cases H; reflexivity.
+qed.
+
+axiom decT : ∀a,b:T. a = b ∨ a ≠ b.
+
+lemma nu : ∀a,b:T. ∀E:a=b. a=b.
+intros (a b E); cases (decT a b) (Ecanonical Abs); [ exact H | cases (H E) ]
 qed.
 
+lemma nu_k : ∀a,b:T. ∀E1,E2:a=b. nu ? ? E1 = nu ? ? E2.
+intros (a b E1 E2); unfold nu; 
+cases (decT a b); simplify; [ reflexivity | cases (H E1) ]
+qed.
+
+definition nu_inv ≝ λa,b:T. λE:a=b. step ? ? ? (nu ? ? (refl_eq ? a)) E. 
+
+definition cancel ≝ λA,B:Type.λf.λg:A→B.∀x:A.f (g x) = x.
+
+lemma cancel_nu_nu_inv : ∀a,b:T. cancel (a=b) (a=b) (nu_inv a b) (nu a b).
+intros (a b); unfold cancel; intros (E); cases E;
+unfold nu_inv; rewrite > stepH; reflexivity.
+qed.
+
+lemma pirrel :  ∀a,b:T.∀E1,E2:a=b. E1 = E2.
+intros (a b E1 E2);
+rewrite < cancel_nu_nu_inv; 
+rewrite < cancel_nu_nu_inv in ⊢ (? ? ? %);
+rewrite > (nu_k ? ? E1 E2).
+reflexivity.
+qed.
+
+(* some more tests *)
 inductive eq4 (A : Type) (x : A) (y : A) : A → A → Prop ≝ 
   eq_refl4 : eq4 A x y x y.
   
@@ -30,4 +61,3 @@ lemma step4 : ∀a,b:T.∀H:eq4 T a b a b.
   eq4_ind T a b (λx,y.eq4 T x y a b) H a b H = eq_refl4 T a b.
 intros (a b H). cases H. reflexivity.
 qed.
-