Commit 97559482 authored by MARCHE Claude's avatar MARCHE Claude

FoVeOOS competition

parent 0d48318f
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
(y <= (Zmax x y))%Z.
Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
((Zmin x y) <= y)%Z.
Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
Inductive tree :=
| Null : tree
| Tree : Z -> tree -> tree -> tree .
Set Implicit Arguments.
Fixpoint mem(v:Z) (t:tree) {struct t}: Prop :=
match t with
| Null => False
| (Tree x l r) => (x = v) \/ ((mem v l) \/ (mem v r))
end.
Unset Implicit Arguments.
Set Implicit Arguments.
Fixpoint ge_tree(v:Z) (t:tree) {struct t}: Prop :=
match t with
| Null => True
| (Tree x l r) => (x <= v)%Z /\ ((ge_tree v l) /\ (ge_tree v r))
end.
Unset Implicit Arguments.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem ge_trans : forall (t:tree) (x:Z) (y:Z), ((y <= x)%Z /\ (ge_tree y
t)) -> (ge_tree x t).
(* YOU MAY EDIT THE PROOF BELOW *)
induction t.
intros; simpl; auto.
intros x y.
simpl.
intros (H,(I,(J,K))).
split; auto with zarith.
split.
apply IHt1 with (y:=y); auto with zarith.
apply IHt2 with (y:=y); auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment