]> matita.cs.unibo.it Git - helm.git/commitdiff
1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 17:58:54 +0000 (17:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 17:58:54 +0000 (17:58 +0000)
   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).

components/cic_unification/cicRefine.ml
matita/tests/coercions_propagation.ma
matita/tests/coercions_russell.ma

index e3e92d098f0f4ed34935543f7a666ec5bb246475..bb978a4cce3b2eef43b4a389ff0243e31d8ffbac 100644 (file)
@@ -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
index 8ff8f9c759ba41d26541571040df79e6b11586af..ce8f2e2a7af943c4ef1ba0520bd45b5cd732a295 100644 (file)
@@ -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
index 50bf81dfd44647c6970923381b708c168175d3ef..f504cef72e9e2a97576892e4d9d003c28df95722 100644 (file)
@@ -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