Commit d78d2472 authored by charguer's avatar charguer

init

parents
% CFML : a characteristic formula generator for OCaml
% Arthur Charguéraud, with contributions from others.
% License : GNU GPL v3.
To view this file in html format, run:
pandoc README.md -o README.html
Description
===========
CFML consists of two parts:
- a tool, implemented in OCaml, which parses OCaml source code
and generates Coq files containing characteristic formulae;
- a Coq library, which exports definitions, lemmas and tactics
used to manipulate characteristic formulae.
(*-- bug 1
Require Import Why3.
Require Import JMeq.
Axiom JMeq_sym : forall (A B : Type) (x : A) (y : B),
JMeq x y -> JMeq y x.
Lemma test_true_1 : True.
Proof. why3 "alt-ergo". Qed.
Anomaly: File "src/coq-tactic/why3tac.ml", line 645, characters 10-16: Assertion failed.
Please report.
-*)
(*-- bug 2
Require Import Why3.
Record R (A:Type) := {
R_hyp : A;
R_ext : R_hyp = R_hyp }.
Lemma test_true_2 : True.
Proof. why3 "alt-ergo". Qed.
Anomaly: File "src/coq-tactic/why3tac.ml", line 560, characters 20-26: Assertion failed.
Please report.
*)
(**********************************************************)
Set Implicit Arguments.
Require Import Why3.
Ltac ae := intros; why3 "alt-ergo" timelimit 1.
(**********************************************************)
(** CFML environment -- LATER *)
Module LibCFTest.
End LibCFTest.
(**********************************************************)
(** Coq environment *)
Module LibCoqTest.
(*--------------------------------------------------------*)
(** Z *)
Require Export ZArith.
Open Scope Z_scope.
Lemma test_Z_1 : forall (x y : Z),
x > 0 -> y > 0 -> x * y > 0.
Proof. ae. Qed.
Lemma test_Z_2 : forall (x y : Z),
x + y > 0 -> x - y < 0 -> y > 0.
Proof. ae. Qed.
Lemma test_Z_3 : forall x,
(forall a, x > a) -> False.
Proof. ae. Qed.
Lemma test_Z_4 : forall x,
(forall a, x > a+1) -> False.
Proof. try ae. Admitted.
(*--------------------------------------------------------*)
(** list *)
Require Export List.
Lemma test_list_1 : forall (x y : nat),
x::y::nil <> nil.
Proof. ae. Qed.
Lemma test_list_2 : forall (L : list nat) a,
L <> nil -> (length (a :: L) > 1)%nat.
Proof. try ae. Admitted. (* a bit slow *)
Lemma test_list_3 : forall (x y : list nat),
x <> nil -> x ++ y <> nil.
Proof. try ae. Admitted.
Lemma test_list_4 : forall (x : list nat),
x <> nil -> exists a y, x = a::y.
Proof. try ae. Admitted.
Lemma test_list_5 : forall (x : list Type),
x <> nil -> x <> nil.
Proof. try ae. Admitted.
(*--------------------------------------------------------*)
(** map *)
Require Import Map.
Lemma test_map_1 : forall (t : map Z Z) (i v:Z),
Map.get t i = v.
Proof. try ae. Admitted. (* todo *)
Lemma test_map_2 : forall (t : map Z Z) (i v:Z),
Map.get (Map.set t i v) i = v.
Proof. try ae. Admitted. (* todo *)
End LibCoqTest.
(**********************************************************)
(** LibCore environment *)
Module LibCoreTest.
(*--------------------------------------------------------*)
(** [Lib*] *)
Require Import LibTactics.
Lemma test_true_1 : True.
Proof. ae. Qed.
Require Import LibAxioms.
Lemma test_quantifiers_1 : forall (P : Prop),
P -> P.
Proof. try ae. Admitted. (* todo: could be first order, see below *)
Module TestQuantifiers.
Parameter (P : Prop).
Lemma test_quantifiers_2 : P -> P.
Proof. ae. Qed.
End TestQuantifiers.
Require Import CFWhyDemosExt.
(* ********************************************************************** *)
(** * General definition of extensionality *)
(** The property [Extensional A] captures the fact that the type [A]
features an extensional equality, in the sense that to prove the
equality between two values of type [A] it suffices to prove that
those two values are related by some binary relation. *)
Class Extensional (A:Type) := {
extensional_hyp : A -> A -> Prop;
extensional : forall x y : A, extensional_hyp x y -> x = y }.
Lemma test_true_2 : True.
Proof. ae. Qed.
Lemma test_partial_eq : forall (x:nat),
(= x) x.
Proof. ae. Qed.
Anomaly: File "src/coq-tactic/why3tac.ml", line 560, characters 20-26: Assertion failed.
Please report.
assert false (* ensured by Coq typing *)
Require Import LibEqual.
Lemma test_true_2 : True.
Proof. ae. Qed.
Lemma test_true_2 : True.
Proof. ae. Qed.
(* coqc CFWhyDemosExt.v -I tlc *)
(* ********************************************************************** *)
(** * General definition of extensionality *)
(** The property [Extensional A] captures the fact that the type [A]
features an extensional equality, in the sense that to prove the
equality between two values of type [A] it suffices to prove that
those two values are related by some binary relation. *)
Class Extensional (A:Type) := {
extensional_hyp : A -> A -> Prop;
extensional : forall x y : A, extensional_hyp x y -> x = y }.
(**************************************************************************)
(** Auxiliary definitions for arrays *)
predicate index (n:int) (i:int) =
0 <= i /\ i < n
(* pas utilis dans ce fichier, mais utile en gnral :
predicate array_index (t:'a farray) (i:int) =
index (farray_length t) i
*)
type tab = int array
(**************************************************************************)
(** Goal 1 from sparse arrays *)
goal sparse_array_1 :
forall (s:int) (n:int) (idx:tab) (back:tab) (i:int) (j:int),
(length idx = s) ->
(length back = s) ->
(index s n) ->
(i <> j) ->
(0 <= n /\ n < s) ->
(index s j) ->
( (index n (idx[j]) /\ back[idx[j]] = j)
<-> ((index n (idx[j]) \/ idx[j] = n) /\ back[n<-i][idx[j]] = j))
(* Hint: start with a case analysis on (index n (Idx[j])) *)
(**************************************************************************)
(** Goal 2 from sparse arrays *)
predicate good_sizes (s:int) (n:int) (back:tab) (idx:tab) (val:tab) :=
length val = s /\ length idx = s /\ length back = s /\ 0 <= n /\ n <= s.
predicate back_correct (s:int) (n:int) (back:tab) (idx:tab) =
forall (k:int),
index n k ->
let i = back[k] in
index s i
/\ idx[i] = k
goal sparse_array_2 :
forall (s : int) (i:int) (v:int) (back:tab) (idx:tab) (n:int) (val:tab),
(index s i) ->
(good_sizes s n back idx val) ->
(back_correct s n back idx) ->
(forall (k:int), index n k -> i <> back[k]) ->
(n < s) ->
(0 <= n < s) ->
(index s n) ->
(index (n + 1) k) ->
index s (back[n<-i][k])
/\ (idx[i<-n][back[n<-i][k]] = k
(* Hint: start with a case analysis on (k = n) *)
(**************************************************************************)
(** Goal 3 from sparse arrays *)
(* Remarque: le "If-then-else" que j'utilise est celui de la logique
classique. Ma dfinition dans Coq est:
Notation "'If' P 'then' v1 'else' v2" := (if classicType P then v1 else v2)
Dans le cas particulier o v1 et v2 sont de type Prop, comme c'est le cas
ci-dessous, on peut encoder cela assez simplement:
Notation "'If' P 'then' Q1 'else' Q2" := ((P /\ Q1) \/ (~ P /\ Q2))
*)
predicate valid (s:int) (n:int) (back:tab) (idx:tab) (i:int) =
index s i
/\ let k = idx[i] in
index n k
/\ back[k] = i
(* Remarque: ci-dessous, "f" est un prdicat abstrait pour la preuve;
on peut le sortir de la quantification si on veut en rajoutant
"axiom f : int -> int" l'extrieur, mais l encore je prfrerais
que cette transformation soit faite la vole. *)
(* Remarque: ci-dessous, si on est oblig, on pourrait encoder l'hypothse:
(f k) = (If P then val[k] else 0)
sous la forme:
If P then (f k = val[k]) else (f k = 0)
et de mme on pourrait encoder la conclusion en extirpant les "If"
au top-level (au dtrimnet de la taille de l'nonc).
*)
goal sparse_array_3 :
forall (s:int) (i:int) (v:int) (f:int->int) (back:tab) (idx:tab) (n:int) (val:tab) (j:int),
(index s i) ->
(good_sizes s n back idx val) ->
(back_correct s n back idx) ->
(forall (k:int), (f k) = (If (valid s n back idx k) then val[k] else 0)) ->
(valid s n back idx i) ->
(If (i = j) then v else (f j))
= (If (valid s n back idx j) then val[i<-v][j] else 0)
(**************************************************************************)
(** Notation for finite sets *)
(* Ces notations peuvent tre inlins si on veut, mais dans ce cas
les buts deviendront vite compltement illisibles. *)
Notation "\{}" := (fset_empty)
Notation "\{ x }" := (fset_single x)
Notation "s1 '\u' s2" := (fset_union s1 s2)
Notation "s1 '\c' s2" := (fset_inclusion s1 s2)
Notation "x '\in' s" := (fset_in x s)
predicate set_notin (x:'a) (s:'a fset) = not (fset_in x e)
Notation "x '\notin' e" := (set_notin x e)
(**************************************************************************)
(** Permutation on sets (used in CFML library) *)
goal fset_permut_1 : forall (x:'a) s1 s2 s3,
(s1 \u \{x} \u (s3 \u \{}) \u s2)
= (s1 \u \{} \u s2 \u (\{x} \u s3))
goal fset_permut_2 : forall (x:'a) (y:'a) s1 t1 t2 s2 s3,
s1 = t1 \u t2 ->
(s1 \u (\{x} \u s2) \u (\{y} \u s3))
= (\{y} \u (t1 \u s3) \u (t2 \u \{x} \u s2))
(**************************************************************************)
(** Non-membership reasoning on sets (used in locally nameless proofs)*)
goal fset_notin_1 : forall (x:'a) e f g,
x \notin (e \u f) ->
x \notin g ->
x \notin (e \u g)
goal fset_notin_2 : forall (x:'a) y e,
x <> y ->
x \notin e ->
x \notin (e \u \{y})
goal fset_notin_3 : forall (x:'a) y e f,
x \notin (e \u \{y} \u f) ->
x \notin \{y}
/\ y \notin \{x}
/\ x <> y
goal fset_notin_4 : forall (x:'a) y e f g,
x \notin (e \u \{y}) ->
(f \u g) \c e ->
x \notin f
goal fset_notin_5 : forall (x:'a) e1 e2 e3 e4 e5 e6 e7 r8 e9,
x \notin (e1 \u e2 \u e3 \u e4 \u (e5 \u e6 \u (e7 \u e8)) \u e9) ->
x \notin e7
(**************************************************************************)
(** Sets and arithmetics (used in program verification) *)
goal fset_with_arithmetic : forall n m e f,
n + 2 = 5 + m ->
e \c (f \u \{n}) ->
(m + 3) \in f ->
e \c f
(* Propositional logic *)
type person
logic david, nancy: person
logic man: person -> prop
logic woman: person -> prop
predicate man_or_woman(p:person) = man(p) or woman(p)
axiom facts : man(david) and woman(nancy)
goal g1: man_or_woman(david)
(* Quantifiers*)
logic father_of: person, person -> prop
logic mother_of: person, person -> prop
axiom father_man:
forall e,p:person. father_of(p,e) -> man(p)
predicate son_of(e:person, p:person) =
father_of(p,e) or mother_of(p,e)
predicate grandfather_of(gp:person, e:person) =
exists p:person.
father_of(gp,p) and ( father_of(p,e) or mother_of(p,e))
goal g2:
forall gp,p:person. grandfather_of(gp,p) -> man(gp)
goal g3:
forall g,p:person.
grandfather_of(g,p) <->
exists pp:person. father_of(g, pp) and son_of(p,pp)
(* Polymorphic Data Types *)
type 'a list
logic nil: 'a list
logic cons: 'a, 'a list -> 'a list
logic hd: 'a list -> 'a
logic tl: 'a list -> 'a list
axiom construction :
forall l:'a list. l<> nil -> cons(hd(l),tl(l)) = l
axiom hd_cons :
forall x:'a. forall l:'a list. hd(cons(x,l)) = x
axiom tl_cons :
forall x:'a. forall l:'a list. tl(cons(x,l)) = l
goal g4:
forall l:'a list. forall r:('a list) list.
r<>nil -> l = hd(r) -> l<>nil ->
cons(cons(hd(l),tl(l)), tl(r)) = r
(* Free Equality *)
type t1
logic h: 'a -> 'a
logic g: 'a,'a -> 'a
goal g5: forall a,x:t1. h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a
logic x,y,z,t1 : int
logic foo : int, int -> int
goal g6 : y = t1 -> foo(x,y) <> foo(x,z) -> t1 <> z
goal g7 : forall a,b,c : 'a. distinct(a,b,c) -> a <> c
(* Associative and Commutative Symbols *)
logic ac u : int, int -> int
goal g8 : u(1,u(2,u(3,u(4,5)))) = u(u(u(u(5,4),3),2),1)
goal g9 :
forall a,b,c,v,w:int.
u(a,b) = w and u(a,c) = v -> u(b,v) = u(c,w)
goal g10 :
forall x, y, z, a, b, c1, c2, d, e1, e2:int.
u(z-y,b)-a = x and u(b,y+1)=a and z=2*y+1 -> x=0
(* Enumerative and Record Data Types *)
type choice = A | B | C
type 'a t = { a : 'a; b : int }
goal g11 :
forall r : choice t. r.a <> A and r.a <> B -> { r with a = C} = r
(* Polymorphic Arrays *)
goal g12:
forall i,j:int.
forall r:(int,int) farray.
forall m:(int,(int,int) farray) farray.
r = m[i] -> m[i<-r[j<-r[j]]] = m
(* Real Arithmetic *)
logic f: real -> real
goal g1:
forall x,y,u,v,z:real.
u = v and u <= x+y and x+y <= u and v <= z+x+4.2 and z+x+4.2 <= v