From: Claudio Sacerdoti Coen Date: Fri, 15 Jun 2018 14:36:37 +0000 (+0200) Subject: Embarassing bug in eta_eq fixed X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8b634b6e8907bb7c5e1a228ec173fab2b7b6546;p=fireball-separation.git Embarassing bug in eta_eq fixed --- diff --git a/ocaml/simple.ml b/ocaml/simple.ml index aa91996..bfb5ebd 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -13,31 +13,6 @@ type t = | L of t ;; -let delta = L(A(V 0, V 0));; - -let eta_eq' = - let rec aux l1 l2 t1 t2 = match t1, t2 with - | L t1, L t2 -> aux l1 l2 t1 t2 - | L t1, t2 -> aux l1 (l2+1) t1 t2 - | t1, L t2 -> aux (l1+1) l2 t1 t2 - | V a, V b -> a + l1 = b + l2 - | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2 - | _, _ -> false - in aux ;; -let eta_eq = eta_eq' 0 0;; - -(* is arg1 eta-subterm of arg2 ? *) -let eta_subterm u = - let rec aux lev t = eta_eq' lev 0 u t || match t with - | L t -> aux (lev+1) t - | A(t1, t2) -> aux lev t1 || aux lev t2 - | _ -> false - in aux 0 -;; - -(* does NOT lift the argument *) -let mk_lams = fold_nat (fun x _ -> L x) ;; - let string_of_t = let string_of_bvar = let bound_vars = ["x"; "y"; "z"; "w"; "q"] in @@ -57,6 +32,12 @@ let string_of_t = in string_of_term_no_pars 0 ;; + +let delta = L(A(V 0, V 0));; + +(* does NOT lift the argument *) +let mk_lams = fold_nat (fun x _ -> L x) ;; + type problem = { orig_freshno: int ; freshno : int @@ -134,6 +115,25 @@ and lift n = ;; let subst = subst 0 false;; +let eta_eq = + let rec aux t1 t2 = match t1, t2 with + | L t1, L t2 -> aux t1 t2 + | L t1, t2 -> aux t1 (A(lift 1 t2,V 0)) + | t1, L t2 -> aux (A(lift 1 t1,V 0)) t2 + | V a, V b -> a = b + | A(t1,t2), A(u1,u2) -> aux t1 u1 && aux t2 u2 + | _, _ -> false + in aux ;; + +(* is arg1 eta-subterm of arg2 ? *) +let eta_subterm u = + let rec aux lev t = eta_eq u (lift lev t) || match t with + | L t -> aux (lev+1) t + | A(t1, t2) -> aux lev t1 || aux lev t2 + | _ -> false + in aux 0 +;; + let subst_in_problem ((v, t) as sub) p = print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t); let sigma = sub::p.sigma in