Commit 00cc8974 authored by MARCHE Claude's avatar MARCHE Claude

build maze completely proved even the stupid lemma

parent 901711d7
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter ref : forall (a:Type), Type.
Parameter uf : Type.
Parameter repr: uf -> Z -> Z -> Prop.
Parameter size: uf -> Z.
Parameter num: uf -> Z.
Axiom Repr_function_1 : forall (u:uf) (x:Z), ((0%Z <= x)%Z /\
(x < (size u))%Z) -> exists y:Z, ((0%Z <= y)%Z /\ (y < (size u))%Z) /\
(repr u x y).
Axiom Repr_function_2 : forall (u:uf) (x:Z) (y:Z) (z:Z), ((0%Z <= x)%Z /\
(x < (size u))%Z) -> ((repr u x y) -> ((repr u x z) -> (y = z))).
Definition same(u:uf) (x:Z) (y:Z): Prop := forall (r:Z), (repr u x r) <->
(repr u y r).
Definition same_reprs(u1:uf) (u2:uf): Prop := forall (x:Z) (r:Z), (repr u1 x
r) <-> (repr u2 x r).
Axiom OneClass : forall (u:uf), ((num u) = 1%Z) -> forall (x:Z) (y:Z),
((0%Z <= x)%Z /\ (x < (size u))%Z) -> (((0%Z <= y)%Z /\
(y < (size u))%Z) -> (same u x y)).
Parameter graph : Type.
Inductive path : graph -> Z -> Z -> Prop :=
| Path_refl : forall (g:graph) (x:Z), (path g x x)
| Path_sym : forall (g:graph) (x:Z) (y:Z), (path g x y) -> (path g y x)
| Path_trans : forall (g:graph) (x:Z) (y:Z) (z:Z), (path g x y) -> ((path g
y z) -> (path g x z)).
Parameter graph1: graph.
Parameter num_edges: Z.
Axiom mult_le : forall (x:Z) (y:Z) (z:Z), ((x <= y)%Z /\ (0%Z <= z)%Z) ->
((x * z)%Z <= (y * z)%Z)%Z.
Theorem Ineq1 : forall (n:Z) (x:Z) (y:Z), (0%Z <= n)%Z -> (((0%Z <= x)%Z /\
(x < n)%Z) -> (((0%Z <= y)%Z /\ (y < n)%Z) ->
(((x * n)%Z + y)%Z < (n * n)%Z)%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
apply Zle_lt_trans with (((n-1)*n + (n-1))%Z).
auto with zarith.
ring_simplify; omega.
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