 ### gallery: more simplified proofs using induction

parent 6fcf22db
 ... ... @@ -46,6 +46,8 @@ module HoareLogic | even_0 : even 0 | even_odd : forall x:int. even x -> even (x+2) lemma even_noneg: forall x:int. even x -> x >= 0 lemma even_not_odd : forall x:int. even x -> even (x+1) -> false let parity (x: ref int) (y: ref int) ... ...
 (* 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 mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 end. Implicit Arguments contents. Inductive even : Z -> Prop := | even_0 : (even 0%Z) | even_odd : forall (x:Z), (even x) -> (even (x + 2%Z)%Z). Theorem even_not_odd : forall (x:Z), (even x) -> ~ (even (x + 1%Z)%Z). (* YOU MAY EDIT THE PROOF BELOW *) assert (nonneg: forall x:Z, even x -> (x >= 0)%Z). induction 1; auto with *. induction 1. red; intro. inversion H. assert (h: (x = -1)%Z) by omega. absurd (-1 >= 0)%Z. omega. apply nonneg. rewrite <- h; auto. intuition. inversion H0. assert (h: (x = -3)%Z) by omega. absurd (-3 >= 0)%Z. omega. apply nonneg. rewrite <- h; auto. assert (x0 = x+1)%Z by omega. subst x0; auto. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -3,95 +3,113 @@ "http://why3.lri.fr/why3session.dtd"> ... ...
No preview for this file type
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require list.List. Require list.Length. Require list.Mem. Require list.Nth. Require option.Option. Require list.Append. Require list.Reverse. Parameter m: Z. Axiom m_positive : (0%Z < m)%Z. Parameter n: Z. Axiom n_nonnegative : (0%Z <= n)%Z. (* Why3 assumption *) Inductive shuffle {a:Type} {a_WT:WhyType a} : (list a) -> (list a) -> (list a) -> Prop := | Shuffle_nil_left : forall (l:(list a)), ((@shuffle _ _) l nil l) | Shuffle_nil_right : forall (l:(list a)), ((@shuffle _ _) nil l l) | Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), ((@shuffle _ _) a1 b c) -> ((@shuffle _ _) (cons x a1) b (cons x c)) | Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), ((@shuffle _ _) a1 b c) -> ((@shuffle _ _) a1 (cons x b) (cons x c)). Axiom shuffle_nil_nil_nil : forall {a:Type} {a_WT:WhyType a}, (shuffle nil nil nil). Axiom shuffle_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle b a1 c). (* Why3 goal *) Theorem shuffle_length : forall {a:Type} {a_WT:WhyType a}, forall (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (((list.Length.length a1) + (list.Length.length b))%Z = (list.Length.length c)). (* Why3 intros a a_WT a1 b c h1. *) induction 1; unfold Length.length; fold @Length.length; omega. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Set Implicit Arguments. Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil:(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a)))) end. Unset Implicit Arguments. Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall (a:Type), forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall (a:Type), forall (l:(list a)), ((length (reverse l)) = (length l)). Inductive option (a:Type) := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Parameter nth: forall (a:Type), Z -> (list a) -> (option a). Implicit Arguments nth. Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None:(option a))) | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. Parameter m: Z. Axiom m_positive : (0%Z < m)%Z. Parameter n: Z. Axiom n_nonnegative : (0%Z <= n)%Z. Inductive shuffle{a:Type} : (list a) -> (list a) -> (list a) -> Prop := | Shuffle_nil_left : forall (l:(list a)), (shuffle l (Nil:(list a)) l) | Shuffle_nil_right : forall (l:(list a)), (shuffle (Nil:(list a)) l l) | Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle (Cons x a1) b (Cons x c)) | Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle a1 (Cons x b) (Cons x c)). Implicit Arguments shuffle. Axiom shuffle_nil_nil_nil : forall (a:Type), (shuffle (Nil:(list a)) (Nil:(list a)) (Nil:(list a))). (* YOU MAY EDIT THE CONTEXT BELOW *) Hint Constructors shuffle. (* DO NOT EDIT BELOW *) Theorem shuffle_sym : forall (a:Type), forall (a1:(list a)) (b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle b a1 c). (* YOU MAY EDIT THE PROOF BELOW *) induction 1; intuition. Qed. (* DO NOT EDIT BELOW *)
This diff is collapsed.
No preview for this file type
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Parameter set : forall (a:Type), Type. Parameter mem: forall (a:Type), a -> (set a) -> Prop. Implicit Arguments mem. Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2). Implicit Arguments infix_eqeq. Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2). Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) -> (mem x s2). Implicit Arguments subset. Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)). Parameter empty: forall (a:Type), (set a). Set Contextual Implicit. Implicit Arguments empty. Unset Contextual Implicit. Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s). Implicit Arguments is_empty. Axiom empty_def1 : forall (a:Type), (is_empty (empty:(set a))). Parameter add: forall (a:Type), a -> (set a) -> (set a). Implicit Arguments add. Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)). Parameter remove: forall (a:Type), a -> (set a) -> (set a). Implicit Arguments remove. Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)). Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)), (subset (remove x s) s). Parameter union: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments union. Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)). Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments inter. Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)). Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments diff. Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)). Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (subset (diff s1 s2) s1). Parameter cardinal: forall (a:Type), (set a) -> Z. Implicit Arguments cardinal. Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)), (0%Z <= (cardinal s))%Z. Axiom cardinal_empty : forall (a:Type), forall (s:(set a)), ((cardinal s) = 0%Z) <-> (is_empty s). Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z). Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z). Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z. Parameter vertex : Type. Parameter succ: vertex -> (set vertex). Inductive path : vertex -> vertex -> Z -> Prop := | path_empty : forall (v:vertex), (path v v 0%Z) | path_succ : forall (v1:vertex) (v2:vertex) (v3:vertex) (n:Z), (path v1 v2 n) -> ((mem v3 (succ v2)) -> (path v1 v3 (n + 1%Z)%Z)). Axiom path_nonneg : forall (v1:vertex) (v2:vertex) (n:Z), (path v1 v2 n) -> (0%Z <= n)%Z. Axiom path_inversion : forall (v1:vertex) (v3:vertex) (n:Z), (0%Z <= n)%Z -> ((path v1 v3 (n + 1%Z)%Z) -> exists v2:vertex, (path v1 v2 n) /\ (mem v3 (succ v2))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem path_closure : forall (s:(set vertex)), (forall (x:vertex), (mem x s) -> forall (y:vertex), (mem y (succ x)) -> (mem y s)) -> forall (v1:vertex) (v2:vertex) (n:Z), (path v1 v2 n) -> ((mem v1 s) -> (mem v2 s)). (* YOU MAY EDIT THE PROOF BELOW *) induction 2; auto. intuition. eauto. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Parameter set : forall (a:Type), Type. Parameter mem: forall (a:Type), a -> (set a) -> Prop. Implicit Arguments mem. Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2). Implicit Arguments infix_eqeq. Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2). Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) -> (mem x s2). Implicit Arguments subset. Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)). Parameter empty: forall (a:Type), (set a). Set Contextual Implicit. Implicit Arguments empty. Unset Contextual Implicit. Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s). Implicit Arguments is_empty. Axiom empty_def1 : forall (a:Type), (is_empty (empty:(set a))). Parameter add: forall (a:Type), a -> (set a) -> (set a). Implicit Arguments add. Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)). Parameter remove: forall (a:Type), a -> (set a) -> (set a). Implicit Arguments remove. Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)). Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)), (subset (remove x s) s). Parameter union: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments union. Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)). Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments inter. Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)). Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a). Implicit Arguments diff. Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)). Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (subset (diff s1 s2) s1). Parameter cardinal: forall (a:Type), (set a) -> Z. Implicit Arguments cardinal.