(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive option (a:Type) {a_WT:WhyType a} := | None : option a | Some : a -> option a. Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a). Existing Instance option_WhyType. Implicit Arguments None [[a] [a_WT]]. Implicit Arguments Some [[a] [a_WT]]. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). (* Why3 assumption *) Inductive char := | Zero : char | One : char . Axiom char_WhyType : WhyType char. Existing Instance char_WhyType. (* Why3 assumption *) Inductive regexp := | Empty : regexp | Epsilon : regexp | Char : char -> regexp | Alt : regexp -> regexp -> regexp | Concat : regexp -> regexp -> regexp | Star : regexp -> regexp . Axiom regexp_WhyType : WhyType regexp. Existing Instance regexp_WhyType. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(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. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, 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} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, 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} {a_WT:WhyType a}, 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 *) Definition word := (list char). (* Why3 assumption *) Inductive mem1 : (list char) -> regexp -> Prop := | mem_eps : (mem1 (Nil :(list char)) Epsilon) | mem_char : forall (c:char), (mem1 (Cons c (Nil :(list char))) (Char c)) | mem_altl : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem1 w r1) -> (mem1 w (Alt r1 r2)) | mem_altr : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem1 w r2) -> (mem1 w (Alt r1 r2)) | mem_concat : forall (w1:(list char)) (w2:(list char)) (r1:regexp) (r2:regexp), (mem1 w1 r1) -> ((mem1 w2 r2) -> (mem1 (infix_plpl w1 w2) (Concat r1 r2))) | mems1 : forall (r:regexp), (mem1 (Nil :(list char)) (Star r)) | mems2 : forall (w1:(list char)) (w2:(list char)) (r:regexp), (mem1 w1 r) -> ((mem1 w2 (Star r)) -> (mem1 (infix_plpl w1 w2) (Star r))). (* Why3 assumption *) Inductive stream := | mk_stream : (list char) -> stream . Axiom stream_WhyType : WhyType stream. Existing Instance stream_WhyType. (* Why3 assumption *) Definition state(v:stream): (list char) := match v with | (mk_stream x) => x end. (* Why3 goal *) Theorem nil_notin_r1 : ~ (mem1 (Nil :(list char)) (Concat (Star (Alt (Char Zero) (Char One))) (Char One))). red; intro. inversion H. inversion H4. rewrite <- H5 in H0. destruct w1; simpl in H0; discriminate H0. Qed.