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' =
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
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. *)
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
(* {{{ 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 =
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'
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
| 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 *)
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 =
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");
~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
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
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
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.
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
projects / helm.git / commitdiff