Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 001cc047 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

The Coq plug-in rules

parent 098d2591
......@@ -2,26 +2,32 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Require int.Int.
Parameter mark : Type.
(* Why3 assumption *)
Definition unit := unit.
Parameter at1: forall (a:Type), a -> mark -> a.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter map : forall (a:Type) (b:Type), Type.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
......@@ -32,91 +38,101 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
(* Why3 assumption *)
Definition elts (a:Type)(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
(* Why3 assumption *)
Definition length (a:Type)(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
Implicit Arguments length.
(* Why3 assumption *)
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
(* Why3 assumption *)
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
(mk_array (length a1) (set (elts a1) i v)).
Implicit Arguments set1.
(* Why3 assumption *)
Inductive sparse_array (a:Type) :=
| mk_sparse_array : (array a) -> (array Z) -> (array Z) -> Z
-> a -> sparse_array a.
Implicit Arguments mk_sparse_array.
Definition back (a:Type)(u:(sparse_array a)): (array Z) :=
match u with
| mk_sparse_array _ _ back1 _ _ => back1
(* Why3 assumption *)
Definition def (a:Type)(v:(sparse_array a)): a :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x4
end.
Implicit Arguments back.
Implicit Arguments def.
Definition card (a:Type)(u:(sparse_array a)): Z :=
match u with
| mk_sparse_array _ _ _ card1 _ => card1
(* Why3 assumption *)
Definition card (a:Type)(v:(sparse_array a)): Z :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x3
end.
Implicit Arguments card.
Definition def (a:Type)(u:(sparse_array a)): a :=
match u with
| mk_sparse_array _ _ _ _ def1 => def1
(* Why3 assumption *)
Definition back (a:Type)(v:(sparse_array a)): (array Z) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x2
end.
Implicit Arguments def.
Implicit Arguments back.
Definition index (a:Type)(u:(sparse_array a)): (array Z) :=
match u with
| mk_sparse_array _ index1 _ _ _ => index1
(* Why3 assumption *)
Definition index (a:Type)(v:(sparse_array a)): (array Z) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x1
end.
Implicit Arguments index.
Definition values (a:Type)(u:(sparse_array a)): (array a) :=
match u with
| mk_sparse_array values1 _ _ _ _ => values1
(* Why3 assumption *)
Definition values (a:Type)(v:(sparse_array a)): (array a) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x
end.
Implicit Arguments values.
(* Why3 assumption *)
Definition is_elt (a:Type)(a1:(sparse_array a)) (i:Z): Prop :=
((0%Z <= (get1 (index a1) i))%Z /\ ((get1 (index a1) i) < (card a1))%Z) /\
((get1 (back a1) (get1 (index a1) i)) = i).
Implicit Arguments is_elt.
Parameter value: forall (a:Type), (sparse_array a) -> Z -> a.
Parameter value: forall (a:Type), (sparse_array a) -> Z -> a.
Implicit Arguments value.
Axiom value_def : forall (a:Type), forall (a1:(sparse_array a)) (i:Z),
((is_elt a1 i) -> ((value a1 i) = (get1 (values a1) i))) /\ ((~ (is_elt a1
i)) -> ((value a1 i) = (def a1))).
(* Why3 assumption *)
Definition length1 (a:Type)(a1:(sparse_array a)): Z := (length (values a1)).
Implicit Arguments length1.
(* Why3 assumption *)
Definition sa_inv (a:Type)(a1:(sparse_array a)): Prop :=
(((0%Z <= (card a1))%Z /\ ((card a1) <= (length1 a1))%Z) /\
((length1 a1) <= 1000%Z)%Z) /\
......@@ -127,20 +143,30 @@ Definition sa_inv (a:Type)(a1:(sparse_array a)): Prop :=
(get1 (back a1) i)) = i))).
Implicit Arguments sa_inv.
(* Why3 assumption *)
Definition injective(a:(map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) ->
((~ (i = j)) -> ~ ((get a i) = (get a j)))).
(* Why3 assumption *)
Definition surjective(a:(map Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\
((get a j) = i).
(* Why3 assumption *)
Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z).
Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) ->
((range a n) -> (surjective a n)).
(*
Add LoadPath "~/why3/src/coq-plugin".
Declare ML Module "whytac".
Ltac ae := why3 "alt-ergo".
*)
(* Why3 goal *)
Theorem permutation : forall (a:Type), forall (a1:(sparse_array a)),
(sa_inv a1) -> (((card a1) = (length1 a1)) -> forall (i:Z),
((0%Z <= i)%Z /\ (i < (length1 a1))%Z) -> (is_elt a1 i)).
......@@ -151,29 +177,35 @@ intro H; decompose [and] H; clear H.
clear a_values a_def H0 H3 H4.
subst n1 n2.
intros. subst a_card.
assert (inj: injective a_back n0).
red; intros.
red; intro.
generalize (H5 i0 H).
generalize (H5 j H1).
intuition.
apply H2.
rewrite <- H11.
rewrite <- H12.
apply f_equal; assumption.
assert (rng: range a_back n0).
red; intros.
generalize (H5 i0); intuition.
assert (inj: injective a_back n0) (* by ae *).
red; intros.
red; intro.
generalize (H5 i0 H).
generalize (H5 j H1).
intuition.
apply H2.
rewrite <- H11.
rewrite <- H12.
apply f_equal; assumption.
assert (rng: range a_back n0) (* by ae *).
red; intros.
generalize (H5 i0); intuition.
generalize (injective_surjective a_back n0 inj rng); intro surj.
destruct (surj i H0) as (j, (hj1, hj2)).
generalize (H5 j hj1); intros (hi1, hi2).
split.
rewrite <- hj2.
rewrite hi2; auto.
rewrite <- hj2.
generalize (H5 j hj1); intuition.
rewrite H8; auto.
(* ae. *)
generalize (H5 j hj1); intros (hi1, hi2).
split.
rewrite <- hj2.
rewrite hi2; auto.
rewrite <- hj2.
generalize (H5 j hj1); intuition.
rewrite H8; auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -7,8 +7,41 @@ Ltac ae := why3 "alt-ergo".
Ltac Z3 := why3 "z3-2".
Ltac spass := why3 "spass".
(* Mutually inductive types *)
Inductive tree : Set :=
| Leaf : tree
| Node : Z -> forest -> tree
with forest : Set :=
| Nil : forest
| Cons : tree -> forest -> forest.
Print plus.
Print tree_rect.
Fixpoint tree_size (t:tree) : Z := match t with
| Leaf => 0
| Node _ f => 1 + forest_size f end
with forest_size (f:forest) : Z := match f with
| Nil => 0
| Cons t f => tree_size t + forest_size f end.
Goal tree_size (Node 42 (Cons Leaf Nil)) = 1.
ae.
Qed.
Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1.
ae.
Qed.
Definition t (a:Type) := list a.
(*
Inductive foo : Set :=
| OO : foo
| SS : forall x:nat, p x -> foo
......@@ -17,32 +50,63 @@ with p : nat -> Prop :=
Goal p O.
ae.
*)
Inductive foo : nat -> Prop :=
c : bar O -> foo O
with bar : nat -> Prop :=
d : forall f:nat->nat, bar (f O).
(*
Goal foo O.
ae.
*)
Inductive tree' : Set :=
| Empty' : tree'
| Node' : forest' -> tree'
with forest' : Set :=
| Forest' : (nat -> tree') -> forest'.
(*
Goal forall f: nat ->tree, True.
intros.
ae.
*)
(*
Parameter f : (nat -> nat) -> nat.
Goal f (plus O) = f (plus O).
ae.
Qed.*)
Parameter f: nat -> nat.
Axiom f_def: f O = O.
Goal f (f O) = O.
ae.
Qed.
Variable b:Set.
Section S.
Variable b:Set->Set.
Variable a:Set.
Inductive sorted : list a -> Prop :=
c: sorted (@nil a)
| d: forall x: a, sorted (cons x nil).
cc: sorted (@nil a)
| dd: forall x: a, sorted (cons x nil).
Variable f : a -> a.
Goal True.
ae.
Qed.
Goal forall x: a, f (f x) = f x -> f (f (f x)) = f x.
intros.
ae.
......@@ -54,11 +118,17 @@ Qed.
End S.
Print All.
Goal True.
ae.
Qed.
Print sorted.
Goal sorted _ (@nil nat).
ae.
Qed.
Parameter p: Z -> Prop.
......@@ -80,12 +150,10 @@ Qed.
(* type definitions *)
Definition t := list.
Inductive foobar : Set :=
C : list nat -> foobar.
Inductive foo : Set :=
C : t nat -> foo.
Goal forall x:foo, x=x.
Goal forall x:foobar, x=x.
intros.
ae.
Qed.
......@@ -127,9 +195,9 @@ Qed.
(* function definition *)
Definition f (x:Z) (y:Z) := x+y.
Definition ff (x:Z) (y:Z) := x+y.
Goal f 1 2 = 3.
Goal ff 1 2 = 3.
ae.
Qed.
......@@ -189,32 +257,6 @@ ae.
Qed.
(* Mutually inductive types *)
Inductive tree : Set :=
| Leaf : tree
| Node : Z -> forest -> tree
with forest : Set :=
| Nil : forest
| Cons : tree -> forest -> forest.
Fixpoint tree_size (t:tree) : Z := match t with
| Leaf => 0
| Node _ f => 1 + forest_size f end
with forest_size (f:forest) : Z := match f with
| Nil => 0
| Cons t f => tree_size t + forest_size f end.
Goal tree_size Leaf = 0.
ae.
Qed.
Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1.
ae.
Qed.
(* Polymorphic, Mutually inductive types *)
Inductive ptree (a:Set) : Set :=
......@@ -230,15 +272,15 @@ ae.
Qed.
Definition a := 0+0.
Definition b := a.
Definition bb := a.
Goal b=0.
Goal bb=0.
ae.
Qed.
Goal b=0.
Goal bb=0.
ae.
Qed.
Fixpoint ptree_size (a:Set) (t:ptree a) : Z := match t with
| PLeaf => 0
......
......@@ -143,18 +143,18 @@ let preid_of_id id = Ident.id_fresh (string_of_id id)
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
identifiers n1...nk with the same path as c, if they exist; otherwise
raises Not_found *)
raises NotFO *)
let rec_names_for c =
let mp,dp,_ = Names.repr_con c in
array_map_to_list
(function
| Name id ->
let c' = Names.make_con mp dp (label_of_id id) in
ignore (Global.lookup_constant c');
(* msgnl (Printer.pr_constr (mkConst c')); *)
ignore
(try Global.lookup_constant c' with Not_found -> raise NotFO);
c'
| Anonymous ->
raise Not_found)
raise NotFO)
(* extract the prenex type quantifications i.e.
type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
......@@ -1012,42 +1012,49 @@ let tr_goal gl =
let () = Printexc.record_backtrace true
let is_goal s =
let n = String.length s in
n >= 11 && String.sub s 0 11 = "Unnamed_thm" ||
n >= 9 && String.sub s (n - 9) 9 = "_admitted"
let tr_top_decl = function
| (sp, kn as _oname), Lib.Leaf lobj ->
let dep = empty_dep () in
let env = Global.env () in
let tvm = Idmap.empty in
let bv = Idmap.empty in
let id = Ident.id_fresh (string_of_id (Libnames.basename sp)) in
Format.printf "tr_top_decl: %s@." (string_of_id (Libnames.basename sp));
begin try match Libobject.object_tag lobj with
| "VARIABLE" ->
assert false (*TODO*)
| "CONSTANT" ->
let c = constant_of_kn kn in
Format.printf "ICI@.";
let r = ConstRef c in
let c = constr_of_reference r in
Format.printf "ICI 2 @.";
let ty = type_of env Evd.empty c in
if is_fo_kind ty then
ignore (tr_task_ts (empty_dep ()) env r)
else
let t = type_of env Evd.empty ty in
if is_Set t || is_Type t then
ignore (tr_task_ls (empty_dep ()) env r)
else if is_Prop t then
let f = tr_formula dep tvm bv env ty in
let pr = Decl.create_prsymbol id in
task := Task.add_prop_decl !task Decl.Paxiom pr f
else
raise NotFO
| "INDUCTIVE" ->
() (*TODO*)
| _ ->
()
let bn = basename sp in
let s = string_of_id bn in
(* Format.printf "tr_top_decl: %s @?" s; *)
begin try
if is_goal s then raise NotFO;
let id = Ident.id_fresh s in
let r = match Libobject.object_tag lobj with
| "VARIABLE" ->
(* ignore variables out of sections *)
ignore (try Global.lookup_named bn with Not_found -> raise NotFO);
VarRef bn
| "CONSTANT" -> ConstRef (constant_of_kn kn)
| "INDUCTIVE" -> IndRef (mind_of_kn kn, 0)
| _ -> raise NotFO
in
let c = constr_of_reference r in
let ty = type_of env Evd.empty c in
if is_fo_kind ty then
ignore (tr_task_ts (empty_dep ()) env r)
else
let t = type_of env Evd.empty ty in
if is_Set t || is_Type t then
ignore (tr_task_ls (empty_dep ()) env r)
else if is_Prop t then
let f = tr_formula dep tvm bv env ty in
let pr = Decl.create_prsymbol id in
task := Task.add_prop_decl !task Decl.Paxiom pr f
else
raise NotFO
with NotFO -> ()
end
(* Format.printf "done@." *)
| _, Lib.CompilingLibrary _
| _, Lib.OpenedModule _
| _, Lib.ClosedModule _
......@@ -1062,10 +1069,10 @@ let whytac s gl =
let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
task := Task.use_export None Theory.builtin_theory;
(* add global declarations from module Top *)
List.iter tr_top_decl (Lib.contents_after None);
(* then translate the goal *)
try
(* add global declarations from module Top *)
List.iter tr_top_decl (List.rev (Lib.contents_after None));
(* then translate the goal *)
tr_goal gl;
let cp, drv = get_prover s in
let command = String.concat " " (cp.command :: cp.extra_options) in
......@@ -1085,8 +1092,8 @@ let whytac s gl =
| NotFO ->
error "Not a first order goal"