Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit 412f3e5c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Coq printer: fix printing of mutually recursive types

parent cb272b65
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
Parameter map : forall (a:Type) (b:Type), Type.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {b:Type}, (map a b) -> a -> b.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {b:Type}, (map a b) -> a -> b -> (map a b).
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : 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) = b1).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
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)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, 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 {a:Type} {b:Type}, b -> (map a b).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {b:Type}, forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -49,12 +61,18 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
Parameter mident : Type.
Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
Axiom ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
(* Why3 assumption *)
Definition ident_index(v:ident): Z := match v with
......@@ -66,11 +84,14 @@ Inductive term_node :=
| Tvalue : value -> term_node
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node .
(* Why3 assumption *)
Inductive term :=
| Tbin : term -> operator -> term -> term_node
with term :=
| mk_term : term_node -> Z -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
......@@ -127,6 +148,8 @@ Inductive fmla :=
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive stmt :=
......@@ -136,12 +159,14 @@ Inductive stmt :=
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
(* Why3 assumption *)
Definition type_value(v:value): datatype :=
match v with
| Vvoid => TYunit
| (Vint int1) => TYint
| (Vint int) => TYint
| (Vbool bool1) => TYbool
end.
......@@ -524,12 +549,20 @@ Axiom consequence_rule : forall (p:fmla) (p':fmla) (q:fmla) (q':fmla)
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem assign_rule : forall (p:fmla) (x:mident) (id:ident) (t:term),
(fresh_in_fmla id p) -> (valid_triple (Flet id t (msubst p x id))
(Sassign x t) p).
intros p x id t h1.
red; intros.
inversion H0; subst; clear H0.
inversion H1; subst; clear H1.
inversion H2; subst; clear H2.
ae.
ae.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
Parameter map : forall (a:Type) (b:Type), Type.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {b:Type}, (map a b) -> a -> b.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {b:Type}, (map a b) -> a -> b -> (map a b).
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : 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) = b1).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
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)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, 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 {a:Type} {b:Type}, b -> (map a b).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {b:Type}, forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -49,12 +61,18 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
Parameter mident : Type.
Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
Axiom ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
(* Why3 assumption *)
Definition ident_index(v:ident): Z := match v with
......@@ -66,11 +84,14 @@ Inductive term_node :=
| Tvalue : value -> term_node
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node .
(* Why3 assumption *)
Inductive term :=
| Tbin : term -> operator -> term -> term_node
with term :=
| mk_term : term_node -> Z -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
......@@ -127,6 +148,8 @@ Inductive fmla :=
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive stmt :=
......@@ -136,12 +159,14 @@ Inductive stmt :=
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
(* Why3 assumption *)
Definition type_value(v:value): datatype :=
match v with
| Vvoid => TYunit
| (Vint int1) => TYint
| (Vint int) => TYint
| (Vbool bool1) => TYbool
end.
......@@ -522,11 +547,15 @@ Parameter x: ident.
Parameter y: mident.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem Test55 : ((eval_term (const (Vint 0%Z):(map mident value)) (Cons (x,
(Vint 42%Z)) (Nil :(list (ident* value)%type))) (mk_tbin (mk_tvar x) Oplus
(mk_tvalue (Vint 13%Z)))) = (Vint 55%Z)).
simpl.
ae.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
.
(* Why3 assumption *)
.
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -29,16 +30,27 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
(* Why3 assumption *)
Definition ident := Z.
Axiom refident : Type.
Parameter refident_WhyType : WhyType refident.
Existing Instance refident_WhyType.
Axiom eq_refident_dec : forall (x:refident) (y:refident), (x = y) \/
~ (x = y).
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tderef : refident -> term
| Tbin : term -> operator -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Inductive fmla :=
......@@ -48,42 +60,45 @@ Inductive fmla :=
| Fimplies : fmla -> fmla -> fmla
| Flet : Z -> term -> fmla -> fmla
| Fforall : Z -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
Parameter map : forall (a:Type) (b:Type), Type.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : 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) = b1).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
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)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, 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 (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Definition env := (map Z value).
Definition env := (map refident value).
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Definition stack := (list (Z* value)%type).
......@@ -120,8 +135,7 @@ Axiom get_stack_neq : forall (x:Z) (i:Z) (v:value) (r:(list (Z*
r)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
Fixpoint eval_term(sigma:(map refident value)) (pi:(list (Z* value)%type))
(t:term) {struct t}: value :=
match t with
| (Tvalue v) => v
......@@ -130,11 +144,9 @@ Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
| (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
pi t2))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* value)%type))
Fixpoint eval_fmla(sigma:(map refident value)) (pi:(list (Z* value)%type))
(f:fmla) {struct f}: Prop :=
match f with
| (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
......@@ -149,11 +161,10 @@ Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* value)%type))
(Vbool b)) pi) f1)
| (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
end.
Unset Implicit Arguments.
Parameter subst_term: term -> Z -> Z -> term.
Parameter subst_term: term -> refident -> Z -> term.
Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
Axiom subst_term_def : forall (e:term) (r:refident) (v:Z),
match e with
| ((Tvalue _)|(Tvar _)) => ((subst_term e r v) = e)
| (Tderef x) => ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
......@@ -162,8 +173,18 @@ Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
(subst_term e2 r v)))
end.
Parameter vsubst_term: term -> Z -> term -> term.
Axiom vsubst_term_def : forall (e:term) (v:Z) (t:term),
match e with
| ((Tvalue _)|(Tderef _)) => ((vsubst_term e v t) = e)
| (Tvar x) => ((v = x) -> ((vsubst_term e v t) = t)) /\ ((~ (v = x)) ->
((vsubst_term e v t) = e))
| (Tbin e1 op e2) => ((vsubst_term e v t) = (Tbin (vsubst_term e1 v t) op
(vsubst_term e2 v t)))
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
......@@ -171,19 +192,21 @@ Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
end.
Unset Implicit Arguments.
Axiom eval_subst_term : forall (sigma:(map Z value)) (pi:(list (Z*
value)%type)) (e:term) (x:Z) (v:Z), (fresh_in_term v e) ->
Axiom eval_subst_term : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e:term) (x:refident) (v:Z), (fresh_in_term v e) ->
((eval_term sigma pi (subst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
Axiom eval_term_change_free : forall (t:term) (sigma:(map Z value)) (pi:(list
(Z* value)%type)) (id:Z) (v:value), (fresh_in_term id t) ->
Axiom eval_vsubst_term : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e:term) (v:Z) (va:value), ((eval_term sigma pi
(vsubst_term e v (Tvalue va))) = (eval_term sigma (Cons (v, va) pi) e)).
Axiom eval_term_change_free : forall (t:term) (sigma:(map refident value))
(pi:(list (Z* value)%type)) (id:Z) (v:value), (fresh_in_term id t) ->
((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm e) => (fresh_in_term id e)
......@@ -194,11 +217,9 @@ Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
(fresh_in_fmla id f1))