From: Enrico Tassi Date: Fri, 7 Sep 2007 17:58:54 +0000 (+0000) Subject: 1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty X-Git-Tag: 0.4.95@7852~212 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3695c4b811d7e0d731724ea3fdcdd1fa68b76006;p=helm.git 1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty fix 2. first real-word example in coercions_russel: a certified "find" procedure from the ocaml library Note: removing the (... : Prop) cast from the example, unification fails badly. To be understood and fixed somehow (i.e. with an Uncertain in place of a Failure). --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index e3e92d098..bb978a4cc 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1198,7 +1198,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = (* aux function to add coercions to funclass *) - let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph = + let rec fix_arity metasenv context subst he hetype eaten args_bo_and_ty ugraph = (* {{{ body *) let pristinemenv = metasenv in let metasenv,hetype' = @@ -1228,7 +1228,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let args, remainder = HExtlib.split_nth how_many_args_are_needed args_bo_and_ty in - let args = List.map fst args in + let args = List.map fst (eaten@args) in let x = if args <> [] then match he with @@ -1258,9 +1258,11 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il match HExtlib.list_findopt (fun (metasenv,last,coerc) -> + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); + debug_print (lazy ("Last " ^ CicMetaSubst.ppterm ~metasenv subst last)); + debug_print (lazy ("x " ^ CicMetaSubst.ppterm ~metasenv subst x)); let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last x ugraph in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) @@ -1285,7 +1287,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il try let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = fix_arity - metasenv context subst t tty remainder ugraph + metasenv context subst t tty [] remainder ugraph in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None @@ -1312,7 +1314,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ body *) function | [] -> newargs,subst,metasenv,he,hetype,ugraph - | (hete, hety)::tl -> + | (hete, hety)::tl as rest -> match (CicReduction.whd ~subst context hetype) with | Cic.Prod (n,s,t) -> let arg,subst,metasenv,ugraph = @@ -1327,7 +1329,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = fix_arity pristinemenv context subst he hetype - (newargs@[hete,hety]@tl) ugraph + newargs rest ugraph in eat_prods_and_args metasenv metasenv subst context pristinehe he hetype' @@ -1346,7 +1348,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il else (* this (says CSC) is also useful to infer dependent types *) try - fix_arity metasenv context subst he hetype args_bo_and_ty ugraph + fix_arity metasenv context subst he hetype [] args_bo_and_ty ugraph with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) more_args_than_expected localization_tbl metasenv @@ -1376,6 +1378,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy "coerce_atom_to_something fails since no coercions found")) | CoercGraph.SomeCoercion candidates -> + debug_print (lazy (string_of_int (List.length candidates) ^ " + candidates found")); let uncertain = ref false in let selected = (* HExtlib.list_findopt *) @@ -1383,8 +1387,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il HExtlib.filter_map (fun (metasenv,last,c) -> try + debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ + " <==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last t ugraph in + fo_unif_subst subst context metasenv last t ugraph + in + let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = @@ -1428,6 +1440,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let infty = clean infty subst context in let expty = clean expty subst context in let t = clean t subst context in + debug_print (lazy ("COERCE_TO_SOMETHING: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^ " ==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); match infty, expty, t with | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) -> debug_print (lazy "FIX"); @@ -1698,7 +1714,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il ~metasenv subst coerced context)); (coerced, expty), subst, metasenv, ugraph | _ -> - debug_print (lazy "ATOM"); + debug_print (lazy ("ATOM: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst infty context ^ " ==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); coerce_atom_to_something t infty expty subst metasenv context ugraph in try diff --git a/matita/tests/coercions_propagation.ma b/matita/tests/coercions_propagation.ma index 8ff8f9c75..ce8f2e2a7 100644 --- a/matita/tests/coercions_propagation.ma +++ b/matita/tests/coercions_propagation.ma @@ -119,11 +119,11 @@ letin xxx ≝ ( in aux : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m); [3: apply xxx]; -unfold PN in aux ⊢ %; [cases (aux n2 n3)] autobatch +unfold PN in aux ⊢ %; [cases (aux n2 n3)] autobatch; qed. -(* guarded troppo debole -theorem test5: nat → ∃n. 1 ≤ n. +(* guarded troppo debole *) +theorem test522: nat → ∃n. 1 ≤ n. apply ( let rec aux n : nat ≝ match n with @@ -133,95 +133,8 @@ apply ( in aux : nat → ∃n. 1 ≤ n); -cases name_con; -simplify; - [ autobatch - | cases (aux n); - simplify; - apply lt_O_S - ] -qed. -*) - -(* -theorem test5: nat → ∃n. 1 ≤ n. -apply ( - let rec aux (n : nat) : ∃n. 1 ≤ n ≝ - match n with - [ O => (S O : ∃n. 1 ≤ n) - | S m => (S (aux m) : ∃n. 1 ≤ n) -(* - inject ? (S (eject ? (aux m))) ? *) - ] - in - aux - : nat → ∃n. 1 ≤ n); - [ autobatch - | elim (aux m); - simplify; - autobatch - ] +[ cases (aux n1); simplify; + autobatch +| autobatch]. qed. -Re1: nat => nat |- body[Rel1] : nat => nat -Re1: nat => X |- body[Rel1] : nat => nat : nat => X -Re1: Y => X |- body[Rel1] : nat => nat : Y => X - -nat => nat -nat => X - -theorem test5: (∃n. 2 ≤ n) → ∃n. 1 ≤ n. -apply ( - λk: ∃n. 2 ≤ n. - let rec aux n : eject ? n = eject ? k → ∃n. 1 ≤ n ≝ - match eject ? n return λx:nat. x = eject ? k → ∃n. 1 ≤ n with - [ O ⇒ λH: 0 = eject ? k. - sigma_intro ? ? 0 ? - | S m ⇒ λH: S m = eject ? k. - sigma_intro ? ? (S m) ? - ] - in - aux k (refl_eq ? (eject ? k))); - - -intro; -cases s; clear s; -generalize in match H; clear H; -elim a; - [ apply (sigma_intro ? ? 0); - | apply (sigma_intro ? ? (S n)); - ]. - -apply ( - λk. - let rec aux n : ∃n. 1 ≤ n ≝ - inject ? - (match n with - [ O ⇒ O - | S m ⇒ S (eject ? (aux m)) - ]) ? - in aux (eject ? k)). - - -apply ( - let rec aux n : nat ≝ - match n with - [ O ⇒ O - | S m ⇒ S (aux m) - ] - in - aux -: (∃n. 2 ≤ n) → ∃n. 1 ≤ n); - -qed. - -(* -theorem test5: nat → ∃n. 0 ≤ n. - apply (λn:nat.?); - apply - (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?] - : ∃n. 0 ≤ n); - autobatch. -qed. -*) -*) \ No newline at end of file diff --git a/matita/tests/coercions_russell.ma b/matita/tests/coercions_russell.ma index 50bf81dfd..f504cef72 100644 --- a/matita/tests/coercions_russell.ma +++ b/matita/tests/coercions_russell.ma @@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/test/russell/". include "nat/orders.ma". include "list/list.ma". +include "datatypes/constructors.ma". inductive sigma (A:Type) (P:A → Prop) : Type ≝ sig_intro: ∀a:A. P a → sigma A P. @@ -51,3 +52,91 @@ letin program_spec ≝ intros; cases (H H1); ] exact program_spec. qed. + +definition nat_return := λn:nat. Some ? n. + +coercion cic:/matita/test/russell/nat_return.con. + +definition raise_exn := None nat. + +definition try_with := + λx,e. match x with [ None => e | Some (x : nat) => x]. + +lemma hd : list nat → option nat := + λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ]. + +axiom f : nat -> nat. + +definition bind ≝ λf:nat->nat.λx. + match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)]. + +include "datatypes/bool.ma". +include "list/sort.ma". +include "nat/compare.ma". + +definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p. + +coercion cic:/matita/test/russell/inject_opt.con 0 1. + +definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w]. + +coercion cic:/matita/test/russell/eject_opt.con. + +definition find : + ∀p:nat → bool. + ∀l:list nat. sigma ? (λres:option nat. + match res with + [ None ⇒ ∀y. mem ? eqb y l = true → p y = false + | Some x ⇒ mem ? eqb x l = true ∧ p x = true ]). +letin program ≝ + (λp. + let rec aux l ≝ + match l with + [ nil ⇒ raise_exn + | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ] + ] + in + aux); +apply + (program : ∀p:nat → bool. + ∀l:list nat. ∃res:option nat. + match res with + [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false + | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]); +clear program; + [ cases (aux l1); clear aux; + simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]); + generalize in match H2; clear H2; + cases a; + [ simplify; + intros 2; + apply (eqb_elim y n); + [ intros; + autobatch + | intros; + apply H2; + simplify in H4; + exact H4 + ] + | simplify; + intros; + cases H2; clear H2; + split; + [ elim (eqb n1 n); + simplify; + autobatch + | assumption + ] + ] + | unfold nat_return; simplify; + split; + [ rewrite > eqb_n_n; + reflexivity + | assumption + ] + | unfold raise_exn; simplify; + intros; + change in H1 with (false = true); + destruct H1 + ] +qed. \ No newline at end of file