Commit 6fcf22db by Jean-Christophe Filliâtre

### gallery: more simplified proofs using induction

parent 89ae90be
 ... ... @@ -42,7 +42,7 @@ theory Tree depths d1 t = depths d2 t -> d1 = d2 lemma depths_subtree: forall t1 t2: tree, d1 d2: int, s1: list int. forall t1 "induction" t2: tree, d1 d2: int, s1: list int. depths d1 t1 ++ s1 = depths d2 t2 -> d1 >= d2 lemma depths_unique2: ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) 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. (* Why3 assumption *) 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))). (* Why3 assumption *) 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). (* Why3 assumption *) 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))). (* Why3 assumption *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . (* Why3 assumption *) Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil :(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. (* Why3 goal *) Theorem depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. (* YOU MAY EDIT THE PROOF BELOW *) induction t; simpl. intuition. intro d. clear IHt2. generalize (IHt1 (d+1))%Z as h1; clear IHt1. destruct (depths (d + 1) t1). intuition. simpl. intros; omega. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) 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. (* Why3 assumption *) 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). (* Why3 assumption *) 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))). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) 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))). (* Why3 assumption *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . (* Why3 assumption *) Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil :(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1 t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)). Require Import Why3. Ltac z := why3 "z3" timelimit 5. (* Why3 goal *) Theorem depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d1 t) s1) = (infix_plpl (depths d2 t) s2)) -> (d1 = d2). induction t; simpl. z. z. Qed.
 (* 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.Append. (* Why3 assumption *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree. Axiom tree_WhyType : WhyType tree. Existing Instance tree_WhyType. (* Why3 assumption *) Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (cons d nil) | (Node l r) => (List.app (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (cons x _) => (d <= x)%Z | nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((List.app (depths d t1) s1) = (List.app (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list Z)), ((List.app (depths d1 t) s1) = (List.app (depths d2 t) s2)) -> (d1 = d2). Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1 t) = (depths d2 t)) -> (d1 = d2). Require Import Why3. Ltac z := why3 "z3" timelimit 5. (* Why3 goal *) Theorem depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list Z)), ((List.app (depths d1 t1) s1) = (depths d2 t2)) -> (d2 <= d1)%Z. (* Why3 intros t1 t2 d1 d2 s1 h1. *) induction t1; simpl. z. intros t2 d1 d2 s1. rewrite <- Append.Append_assoc. intro h. assert (d2 <= d1+1)%Z by z. assert (d2 = d1+1 \/ d2 < d1+1)%Z by omega. destruct H0. subst d2. replace (depths (d1+1) t2)%Z with (app (depths (d1+1) t2) nil)%Z in h. assert (t1_1 = t2) by z. z. z. z. Qed.
 (* 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.Append. (* Why3 assumption *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree. Axiom tree_WhyType : WhyType tree. Existing Instance tree_WhyType. (* Why3 assumption *) Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (cons d nil) | (Node l r) => (List.app (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (cons x _) => (d <= x)%Z | nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((List.app (depths d t1) s1) = (List.app (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list Z)), ((List.app (depths d1 t) s1) = (List.app (depths d2 t) s2)) -> (d1 = d2). Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1 t) = (depths d2 t)) -> (d1 = d2). Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list Z)), ((List.app (depths d1 t1) s1) = (depths d2 t2)) -> (d2 <= d1)%Z. Require Import Why3. Ltac z := why3 "z3" timelimit 5. (* Why3 goal *) Theorem depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1 t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)). (* Why3 intros t1 t2 d1 d2 h1. *) intros t1 t2 d1 d2 h. assert (depths d1 t1 = app (depths d1 t1) nil) by z. assert (d1 >= d2)%Z by z. assert (depths d2 t2 = app (depths d2 t2) nil) by z. assert (d1 = d2) by z. z. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) 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. (* Why3 assumption *) 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). (* Why3 assumption *) 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))). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) 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))). (* Why3 assumption *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . (* Why3 assumption *) Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil :(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). (* Why3 assumption *) Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. (* Why3 assumption *) Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop := | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1, y1) (x2, y2)) | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x, y2)). (* Why3 assumption *) 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)). (* Why3 assumption *) Set Implicit Arguments. Fixpoint forest_depths(f:(list (Z* tree)%type)) {struct f}: (list Z) := match f with | Nil => (Nil :(list Z)) | (Cons (d, t) r) => (infix_plpl (depths d t) (forest_depths r)) end. Unset Implicit Arguments. Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z* tree)%type)), ((forest_depths (infix_plpl f1 f2)) = (infix_plpl (forest_depths f1) (forest_depths f2))). (* Why3 assumption *) Set Implicit Arguments. Fixpoint map_leaf(l:(list Z)) {struct l}: (list (Z* tree)%type) := match l with | Nil => (Nil :(list (Z* tree)%type)) | (Cons d r) => (Cons (d, Leaf) (map_leaf r)) end. Unset Implicit Arguments. (* Why3 goal *) Theorem map_leaf_depths : forall (l:(list Z)), ((forest_depths (map_leaf l)) = l). induction l; simpl; auto. rewrite IHl; auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition unit := unit.