diff options
Diffstat (limited to 'test-suite/success/Case9.v')
-rw-r--r-- | test-suite/success/Case9.v | 104 |
1 files changed, 55 insertions, 49 deletions
diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v index a5d07405..a8534a0b 100644 --- a/test-suite/success/Case9.v +++ b/test-suite/success/Case9.v @@ -1,55 +1,61 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). - -Inductive eqlong : (List nat)-> (List nat)-> Prop := - eql_cons : (n,m:nat)(x,y:(List nat)) - (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) -| eql_nil : (eqlong (Nil nat) (Nil nat)). - - -Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). -Parameter V2 : (a:nat)(x:(List nat)) - (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). -Parameter V3 : (a:nat)(x:(List nat)) - (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). -Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) - (eqlong (Cons nat a x)(Cons nat b y)) - \/ ~(eqlong (Cons nat a x) (Cons nat b y)). - -Parameter nff : (n,m:nat)(x,y:(List nat)) - ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)). -Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)). -Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)). - -Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) := -[y:(List nat)] - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Inductive eqlong : List nat -> List nat -> Prop := + | eql_cons : + forall (n m : nat) (x y : List nat), + eqlong x y -> eqlong (Cons nat n x) (Cons nat m y) + | eql_nil : eqlong (Nil nat) (Nil nat). + + +Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat). +Parameter + V2 : + forall (a : nat) (x : List nat), + eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x). +Parameter + V3 : + forall (a : nat) (x : List nat), + eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat). +Parameter + V4 : + forall (a : nat) (x : List nat) (b : nat) (y : List nat), + eqlong (Cons nat a x) (Cons nat b y) \/ + ~ eqlong (Cons nat a x) (Cons nat b y). + +Parameter + nff : + forall (n m : nat) (x y : List nat), + ~ eqlong x y -> ~ eqlong (Cons nat n x) (Cons nat m y). +Parameter + inv_r : forall (n : nat) (x : List nat), ~ eqlong (Nil nat) (Cons nat n x). +Parameter + inv_l : forall (n : nat) (x : List nat), ~ eqlong (Cons nat n x) (Nil nat). + +Fixpoint eqlongdec (x y : List nat) {struct x} : + eqlong x y \/ ~ eqlong x y := + match x, y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons a x as L1, Cons b y as L2 => + match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with + | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) + | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) end - end. + end. Type - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons a x as L1, Cons b y as L2 => + match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with + | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) + | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) end - end. + end. |