Require Import Why3. Inductive Why3Unhabited : Prop := . Axiom letUsTrustWhy3 : Why3Unhabited. Ltac ae := why3 "alt-ergo" timelimit 5 ; case letUsTrustWhy3. Ltac z3 := why3 "z3" timelimit 5; case letUsTrustWhy3. Require Export ZArith. Open Scope Z_scope. Require Export Lists.List. Section S0. Variable a:Set->Set. Goal forall b:Set->Set, forall x:a nat, x=x. intros; ae. Qed. Goal forall f: (nat->nat)->nat, f S = O -> True. intros; ae. Qed. End S0. (* Mutually inductive types *) Inductive tree : Set := | Leaf : tree | Node : Z -> forest -> tree with forest : Set := | Nil : forest | Cons : tree -> forest -> forest. Fixpoint tree_size (t:tree) : Z := match t with | Leaf => 0 | Node _ f => 1 + forest_size f end with forest_size (f:forest) : Z := match f with | Nil => 0 | Cons t f => tree_size t + forest_size f end. Goal tree_size (Node 42 (Cons Leaf Nil)) = 1. ae. Qed. Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1. ae. Qed. Inductive foo : Set := | OO : foo | SS : forall x:nat, p x -> foo with p : nat -> Prop := | cc : p O. Goal p O. (* not a first order goal *) try ae. exact cc. Qed. Inductive fooo : nat -> Prop := c : bar O -> fooo O with bar : nat -> Prop := d : forall f:nat->nat, bar (f O). Goal fooo O. (* Don't know *) try ae. exact (c (d (fun x => O))). Qed. Inductive tree' : Set := | Empty' : tree' | Node' : forest' -> tree' with forest' : Set := | Forest' : (nat -> tree') -> forest'. Goal forall f: nat ->tree, True. intros. ae. Qed. Parameter f : (nat -> nat) -> nat. Goal f (plus O) = f (plus O). (* not a first order goal *) try ae. trivial. Qed. Parameter f' : nat -> nat. Axiom f'_def: f' O = O. Goal f' (f' O) = O. ae. Qed. Variable b:Set. Section S. Variable b:Set->Set. Variable a:Set. Inductive sorted : list a -> Prop := ccc: sorted (@nil a) | ddd: forall x: a, sorted (cons x nil). Variable f : a -> a. Goal True. ae. Qed. Goal forall x: a, f (f x) = f x -> f (f (f x)) = f x. intros. ae. Qed. Goal forall l: list a, l=l. ae. Qed. End S. Goal True. ae. Qed. Parameter par: Z -> Prop. (* let in *) Goal let t := Z in let f := par 0 in (forall x:t, par x -> par (let y := x+1 in y)) -> f -> par 1. ae. Qed. (* cast *) Goal ( (forall x:Z, par x -> par (x+1)) -> par (0 : Z) -> par 1 : Prop). ae. Qed. (* type definitions *) Parameter t : Set -> Set. Inductive foobar : Set := C : t nat -> foobar. Goal forall x:foobar, x=x. intros. ae. Qed. (* predicate definition *) Definition p' (x:nat) := x=O. Goal p' O. ae. Qed. Goal plus O O = O. ae. Qed. Definition eq' (A:Set) (x y : A) := x=y. Goal eq' nat O O. ae. Qed. Definition pred (n:nat) := match n with | O => O | S p => p end. Goal pred (S O) = O. ae. Qed. (* function definition *) Definition ff (x:Z) (y:Z) := x+y. Goal ff 1 2 = 3. ae. Qed. Definition id A (x:A) := x. Goal id nat O = O. ae. Qed. (* recursive function definition *) Goal length (cons 1 (cons 2 nil)) = S (S O). ae. Qed. (* recursive predicate definition *) Goal In 0 (cons 1 (cons 0 nil)). ae. Qed. (* inductive types *) Parameter P : (nat -> nat) -> Prop. Goal forall (a:Set), forall x:nat, x=S O -> P S -> let y := (S (S O)) in S x=y. intros. ae. Qed. Goal forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y. intros. ae. Qed. Goal forall x: list nat, x=x. intros. ae. Qed. Goal (match (S (S (S O))) with (S (S _)) => True | _ => False end). ae. Qed. Goal forall a, forall (x: list (list a)), 1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2. intros a x. assert (x=nil \/ exists y: list a, exists z:list (list a), x = cons y z). destruct x; ae. ae. Qed. (* Polymorphic, Mutually inductive types *) Inductive ptree {a:Set} : Set := | PLeaf : ptree | PNode : a -> pforest -> ptree with pforest {a:Set} : Set := | PNil : pforest | PCons : ptree -> pforest -> pforest. Goal forall x : @ptree Z, x=x. ae. Qed. Definition a := 0+0. Definition bb := a. Goal bb=0. ae. Qed. Goal bb=0. ae. Qed. Fixpoint ptree_size {a:Set} (t:@ptree a) : Z := match t with | PLeaf => 0 | PNode _ f => 1 + pforest_size f end with pforest_size {a:Set} (f:@pforest a) : Z := match f with | PNil => 0 | PCons t f => ptree_size t + pforest_size f end. Goal ptree_size (@PLeaf Z) = 0. ae. Qed. Goal forall (a:Set), ptree_size (@PLeaf a) = 0. intros. ae. Qed. (* the same, without parameters *) Inductive ptree' : Type -> Type := | PLeaf' : forall (a:Type), ptree' a | PNode' : forall (a:Type), a -> pforest' a -> ptree' a with pforest' : Type -> Type := | PNil' : forall (a:Type), pforest' a | PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a. Goal forall x : ptree' Z, x=x. ae. Qed. (* order of type parameters matters *) Definition wgt (k:(nat * Z)%type) := match k with | (_, p) => p end. Implicit Arguments wgt. Goal wgt (S O, 3) = 3. ae. Qed. Require Import Rbase. Require Import R_sqrt. Require Import Rfunctions. Require Import Rbasic_fun. Goal forall (x:R), (0 <= x * x)%R. ae. Qed.