From 30392d5cb910fae96eee91ae30cebfb864be41db Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 28 Feb 2006 15:36:03 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/dp/.cvsignore | 2 + contrib/dp/TODO | 28 +++++++++++ contrib/dp/dp.ml | 126 ++++++++++++++++++-------------------------------- contrib/dp/dp_why.ml | 50 ++++++++++++-------- contrib/dp/test2.v | 73 +++++++++++++++++++++++++++++ contrib/dp/tests.v | 14 +++--- 6 files changed, 187 insertions(+), 106 deletions(-) create mode 100644 contrib/dp/.cvsignore create mode 100644 contrib/dp/TODO create mode 100644 contrib/dp/test2.v (limited to 'contrib/dp') diff --git a/contrib/dp/.cvsignore b/contrib/dp/.cvsignore new file mode 100644 index 000000000..27102315a --- /dev/null +++ b/contrib/dp/.cvsignore @@ -0,0 +1,2 @@ +test.why +test_why* diff --git a/contrib/dp/TODO b/contrib/dp/TODO new file mode 100644 index 000000000..387cacdf3 --- /dev/null +++ b/contrib/dp/TODO @@ -0,0 +1,28 @@ + +TODO +---- + +- axiomes pour les prédicats récursifs comme + + Fixpoint even (n:nat) : Prop := + match n with + O => True + | S O => False + | S (S p) => even p + end. + + ou encore In sur les listes du module Coq List. + +- discriminate + +- inversion (Set et Prop) + + +BUGS +---- + +- value = Some : forall A:Set, A -> option A + + -> eta_expanse échoue sur assert false (ligne 147) + + diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index a9d450f75..6f6a5a803 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -231,19 +231,35 @@ let term_abstractions = Hashtbl.create 97 let new_abstraction = let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r -(* translates a Coq term p:positive into a FOL term of type int *) -let rec fol_term_of_positive tv env p = - match kind_of_term p with - | Term.Construct _ when p = Lazy.force coq_xH -> - Cst 1 - | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> - Plus (Mult (Cst 2, (fol_term_of_positive tv env a)), Cst 1) - | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> - Mult (Cst 2, (fol_term_of_positive tv env a)) - | Var id -> - Fol.App (string_of_id id, []) - | _ -> - tr_term tv [] env p +(* Arithmetic constants *) + +exception NotArithConstant + +(* translates a closed Coq term p:positive into a FOL term of type int *) +let rec tr_positive p = match kind_of_term p with + | Term.Construct _ when p = Lazy.force coq_xH -> + Cst 1 + | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> + Plus (Mult (Cst 2, tr_positive a), Cst 1) + | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> + Mult (Cst 2, tr_positive a) + | Term.Cast (p, _, _) -> + tr_positive p + | _ -> + raise NotArithConstant + +(* translates a closed Coq term t:Z into a FOL term of type int *) +let rec tr_arith_constant t = match kind_of_term t with + | Term.Construct _ when t = Lazy.force coq_Z0 -> + Cst 0 + | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> + tr_positive a + | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> + Moins (Cst 0, tr_positive a) + | Term.Cast (t, _, _) -> + tr_arith_constant t + | _ -> + raise NotArithConstant (* translate a Coq term t:Set into a FOL type expression; tv = list of type variables *) @@ -272,54 +288,6 @@ and tr_type tv env t = raise NotFO end -(**** OLD TR_TYPE - else if is_Prop ty then [], Tid ("BOOLEAN", []) - else if is_Set ty then [], Tid ("TYPE", []) - else if is_imp_term ty then - begin match match_with_imp_term ty with - | Some (t1, t2) -> begin match tr_type tv env t1, tr_type tv env t2 with - | ([], t1'), (l2, t2') -> t1' :: l2, t2' - | _ -> raise NotFO - end - | _ -> assert false - end - else - try let r = global_of_constr ty in - (try - begin match lookup_global r with - | DeclType (id,0) -> [], Tid (id,[]) - | _ -> assert false (* assumption: t:Set *) - end - with Not_found -> - begin match r with - | IndRef i -> - let id = rename_global r in - let d = DeclType (id,0) in - add_global r (Gfo d); - globals_stack := d :: !globals_stack; - iter_all_constructors i - (fun _ c -> - let rc = global_of_constr c in - try - begin match tr_global env rc with - | DeclFun (idc, [], _) -> () - | DeclFun (idc, al, _) -> injection idc al - | _ -> assert false - end - with NotFO -> - ()); - [], Tid (id,[]) - | _ -> - let id = rename_global r in - let d = DeclType (id,0) in - add_global r (Gfo d); - globals_stack := d :: !globals_stack; - [], Tid (id,[]) - (* TODO: constant type definition *) - end) - with Not_found -> raise NotFO -***) - and make_term_abstraction tv env c = let ty = Typing.type_of env Evd.empty c in let id = new_abstraction () in @@ -404,6 +372,7 @@ and axiomatize_body env r id d = match r with let value = tr_term tv [] env b in [id, Fatom (Eq (Fol.App (id, []), value))] | DeclFun (id, _, l, _) | DeclPred (id, _, l) -> + Format.eprintf "axiomatize_body %S@." id; let b = match kind_of_term b with (* a single recursive function *) | Fix (_, (_,_,[|b|])) -> @@ -528,27 +497,22 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with | _ -> raise NotFO - (* assumption: t:T:Set *) -and tr_term tv bv env t = - match kind_of_term t with - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> - Plus (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> - Moins (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> - Mult (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> - Div (tr_term tv bv env a, tr_term tv bv env b) - | Term.Construct _ when t = Lazy.force coq_Z0 -> - Cst 0 - | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> - fol_term_of_positive tv env a - | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - Moins (Cst 0, (fol_term_of_positive tv env a)) - | Term.Var id when List.mem id bv -> - App (string_of_id id, []) - | _ -> +and tr_term tv bv env t = match kind_of_term t with + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> + Plus (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> + Moins (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> + Mult (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> + Div (tr_term tv bv env a, tr_term tv bv env b) + | Term.Var id when List.mem id bv -> + App (string_of_id id, []) + | _ -> + try + tr_arith_constant t + with NotArithConstant -> let f, cl = decompose_app t in begin try let r = global_of_constr f in diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml index d6a5e145c..662a5a8be 100644 --- a/contrib/dp/dp_why.ml +++ b/contrib/dp/dp_why.ml @@ -12,16 +12,28 @@ let rec print_list sep print fmt = function let space fmt () = fprintf fmt "@ " let comma fmt () = fprintf fmt ",@ " -let is_why_keyword s = false (* TODO *) +let is_why_keyword = + let h = Hashtbl.create 17 in + List.iter + (fun s -> Hashtbl.add h s ()) + ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin"; + "bool"; "do"; "done"; "else"; "end"; "exception"; "exists"; + "external"; "false"; "for"; "forall"; "fun"; "function"; "goal"; + "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not"; + "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises"; + "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try"; + "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; + Hashtbl.mem h let ident fmt s = - if is_why_keyword s then fprintf fmt "why__%s" s else fprintf fmt "%s" s + if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s let rec print_typ fmt = function - | Tvar x -> fprintf fmt "'%s" x - | Tid (x, []) -> fprintf fmt "%s" x - | Tid (x, [t]) -> fprintf fmt "%a %s" print_typ t x - | Tid (x, tl) -> fprintf fmt "(%a) %s" (print_list comma print_typ) tl x + | Tvar x -> fprintf fmt "'%a" ident x + | Tid ("int", []) -> fprintf fmt "int" + | Tid (x, []) -> fprintf fmt "%a" ident x + | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x + | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x let rec print_term fmt = function | Cst n -> @@ -79,40 +91,42 @@ let rec print_predicate fmt p = let print_query fmt (decls,concl) = let print_dtype = function | DeclType (id, 0) -> - fprintf fmt "@[type %s@]@\n@\n" id + fprintf fmt "@[type %a@]@\n@\n" ident id | DeclType (id, 1) -> - fprintf fmt "@[type 'a %s@]@\n@\n" id + fprintf fmt "@[type 'a %a@]@\n@\n" ident id | DeclType (id, n) -> fprintf fmt "@[type ("; - for i = 1 to n do fprintf fmt "'a%d" i done; - fprintf fmt ") %s@]@\n@\n" id + for i = 1 to n do + fprintf fmt "'a%d" i; if i < n then fprintf fmt ", " + done; + fprintf fmt ") %a@]@\n@\n" ident id | DeclFun _ | DeclPred _ | Axiom _ -> () in let print_dvar_dpred = function | DeclFun (id, _, [], t) -> - fprintf fmt "@[logic %s : -> %a@]@\n@\n" id print_typ t + fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t | DeclFun (id, _, l, t) -> - fprintf fmt "@[logic %s : %a -> %a@]@\n@\n" - id (print_list comma print_typ) l print_typ t + fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" + ident id (print_list comma print_typ) l print_typ t | DeclPred (id, _, []) -> - fprintf fmt "@[logic %s : -> prop @]@\n@\n" id + fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id | DeclPred (id, _, l) -> - fprintf fmt "@[logic %s : %a -> prop@]@\n@\n" - id (print_list comma print_typ) l + fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" + ident id (print_list comma print_typ) l | DeclType _ | Axiom _ -> () in let print_assert = function | Axiom (id, f) -> - fprintf fmt "@[axiom %s:@ %a@]@\n@\n" id print_predicate f + fprintf fmt "@[axiom %a:@ %a@]@\n@\n" ident id print_predicate f | DeclType _ | DeclFun _ | DeclPred _ -> () in List.iter print_dtype decls; List.iter print_dvar_dpred decls; List.iter print_assert decls; - fprintf fmt "@[goal coq__goal: %a@]" print_predicate concl + fprintf fmt "@[goal coq___goal: %a@]" print_predicate concl let output_file f q = let c = open_out f in diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v new file mode 100644 index 000000000..59f8807f9 --- /dev/null +++ b/contrib/dp/test2.v @@ -0,0 +1,73 @@ +Require Import ZArith. +Require Import Classical. +Require Import List. + +Open Scope list_scope. +Open Scope Z_scope. + +Definition neg (z:Z) : Z := match z with + | Z0 => Z0 + | Zpos p => Zneg p + | Zneg p => Zpos p + end. + +Goal forall z, neg (neg z) = z. + zenon. + Admitted. + +Open Scope nat_scope. +Print plus. + +Goal forall x, x+0=x. + induction x; zenon. + (* simplify resoud le premier, pas le second *) + Admitted. + +Goal 1::2::3::nil = 1::2::(1+2)::nil. + zenon. + Admitted. + +Fixpoint even (n:nat) : Prop := + match n with + O => True + | S O => False + | S (S p) => even p + end. + +Goal even 4%nat. + zenon. + Admitted. + +Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil. + +Definition head := +fun (A : Set) (l : list A) => +match l with +| nil => None (A:=A) +| x :: _ => Some x +end. + +Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1. + +zenon. +Admitted. + +(* +BUG avec head prédéfini : manque eta-expansion sur A:Set + +Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1. + +Print value. +Print Some. + +zenon. +*) + +Inductive IN (A:Set) : A -> list A -> Prop := + | IN1 : forall x l, IN A x (x::l) + | IN2: forall x l, IN A x l -> forall y, IN A x (y::l). +Implicit Arguments IN [A]. + +Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l). + zenon. +Print In. diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index 10b6f0d83..222d08cc8 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -1,4 +1,3 @@ -Reset Initial. Require Import ZArith. Require Import Classical. @@ -64,10 +63,11 @@ Goal (forall (x y : Z), x = y) -> 0 = 1. simplify. Qed. +Goal forall (x: nat), (x + 0 = x)%nat. -Goal forall (x y : Z), x + y = y + x. - -induction x ; simplify. +induction x0. +zenon. +zenon. Qed. @@ -98,7 +98,7 @@ simplify. Qed. -(* Inductive types definitions - call to injection function *) +(* Inductive types definitions - call to incontrib/dp/jection function *) Inductive even : Z -> Prop := | even_0 : even 0 @@ -185,9 +185,9 @@ Qed. (* sorts issues *) Parameter foo : Set. -Parameter f : nat -> foo -> foo -> nat. +Parameter ff : nat -> foo -> foo -> nat. Parameter g : foo -> foo. -Goal (forall x:foo, f 0 x x = O) -> forall y, f 0 (g y) (g y) = O. +Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O. simplify. Qed. -- cgit v1.2.3