From 6dd842fc0aede1ea6e345789f7051ce7cfa9c8c2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Apr 2007 08:35:14 +0000 Subject: [PATCH] new case implementation --- .../components/tactics/primitiveTactics.ml | 217 +++++++++--------- .../matita/library/technicalities/setoids.ma | 16 +- helm/software/matita/tests/pirrel.ma | 36 ++- 3 files changed, 147 insertions(+), 122 deletions(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index de68ca053..07723ea9f 100644 --- 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 e589a33d0..0f3bda302 100644 --- 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 e9ff7ca59..15c1a982f 100644 --- 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. - -- 2.39.2