Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ZCoeff.v Sprache: Coq

Original von: Coq^©

(****************************************************************************)
(* Pattern-matching when non inductive terms occur                          *)

(* Dependent form of annotation *)
Type match 0 as n, @eq return nat with
     | O, x => 0
     | S x, y => x
     end.
Type match 0, 0, @eq return nat with
     | O, x, y => 0
     | S x, y, z => x
     end.
Type match 0, @eq, 0 return _ with
     | O, x, y => 0
     | S x, y, z => x
     end.

(* Non dependent form of annotation *)
Type match 0, @eq return nat with
     | O, x => 0
     | S x, y => x
     end.

(* Combining dependencies and non inductive arguments *)
Type
  (fun (A : Set) (a : A) (H : 0 = 0) =>
   match H in (_ = x), a return (H = H) with
   | _, _ => refl_equal H
   end).

(* Interaction with coercions *)
Parameter bool2nat : bool -> nat.
Coercion bool2nat : bool >-> nat.
Definition foo : nat -> nat :=
  fun x => match x with
             | O => true
             | S _ => 0
           end.

(****************************************************************************)
(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v   *)

Inductive IFExpr : Set :=
  | Var : nat -> IFExpr
  | Tr : IFExpr
  | Fa : IFExpr
  | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.

Inductive List (A : Set) : Set :=
  | Nil : List A
  | Cons : A -> List A -> List A.

Inductive listn : nat -> Set :=
  | niln : listn 0
  | consn : forall n : nat, nat -> listn n -> listn (S n).

Inductive Listn (A : Set) : nat -> Set :=
  | Niln : Listn A 0
  | Consn : forall n : nat, nat -> Listn A n -> Listn A (S n).

Inductive Le : nat -> nat -> Set :=
  | LeO : forall n : nat, Le 0 n
  | LeS : forall n m : nat, Le n m -> Le (S n) (S m).

Inductive LE (n : nat) : nat -> Set :=
  | LE_n : LE n n
  | LE_S : forall m : nat, LE n m -> LE n (S m).

Require Import Bool.

Inductive PropForm : Set :=
  | Fvar : nat -> PropForm
  | Or : PropForm -> PropForm -> PropForm.

Section testIFExpr.
Definition Assign := nat -> bool.
Parameter Prop_sem : Assign -> PropForm -> bool.

Type
  (fun (A : Assign) (F : PropForm) =>
   match F return bool with
   | Fvar n => A n
   | Or F G => Prop_sem A F || Prop_sem A G
   end).

Type
  (fun (A : Assign) (H : PropForm) =>
   match H return bool with
   | Fvar n => A n
   | Or F G => Prop_sem A F || Prop_sem A G
   end).
End testIFExpr.

Type (fun x : nat => match x return nat with
                     | O => 0
                     | x => x
                     end).

Module Type testlist.
Parameter A : Set.
Inductive list : Set :=
  | nil : list
  | cons : A -> list -> list.
Parameter inf : A -> A -> Prop.

Definition list_Lowert2 (a : A) (l : list) :=
  match l return Prop with
  | nil => True
  | cons b l => inf a b
  end.

Definition titi (a : A) (l : list) :=
  match l return list with
  | nil => l
  | cons b l => l
  end.
End testlist.

(* To test translation *)
(* ------------------- *)

Type match 0 return nat with
     | O => 0
     | _ => 0
     end.

Type match 0 return nat with
     | O as b => b
     | S O => 0
     | S (S x) => x
     end.

Type match 0 with
     | O as b => b
     | S O => 0
     | S (S x) => x
     end.

Type (fun x : nat => match x return nat with
                     | O as b => b
                     | S x => x
                     end).

Type (fun x : nat => match x with
                     | O as b => b
                     | S x => x
                     end).

Type match 0 return nat with
     | O as b => b
     | S x => x
     end.

Type match 0 return nat with
     | x => x
     end.

Type match 0 with
     | x => x
     end.

Type match 0 return nat with
     | O => 0
     | S x as b => b
     end.

Type (fun x : nat => match x return nat with
                     | O => 0
                     | S x as b => b
                     end).

Type (fun x : nat => match x with
                     | O => 0
                     | S x as b => b
                     end).

Type match 0 return nat with
     | O => 0
     | S x => 0
     end.

Type match 0 return (nat * nat) with
     | O => (0, 0)
     | S x => (x, 0)
     end.

Type match 0 with
     | O => (0, 0)
     | S x => (x, 0)
     end.

Type
  match 0 return (nat -> nat) with
  | O => fun n : nat => 0
  | S x => fun n : nat => 0
  end.

Type match 0 with
     | O => fun n : nat => 0
     | S x => fun n : nat => 0
     end.

Type
  match 0 return (nat -> nat) with
  | O => fun n : nat => 0
  | S x => fun n : nat => x + n
  end.

Type match 0 with
     | O => fun n : nat => 0
     | S x => fun n : nat => x + n
     end.

Type match 0 return nat with
     | O => 0
     | S x as b => b + x
     end.

Type match 0 return nat with
     | O => 0
     | S a as b => b + a
     end.
Type match 0 with
     | O => 0
     | S a as b => b + a
     end.

Type match 0 with
     | O => 0
     | _ => 0
     end.

Type match 0 return nat with
     | O => 0
     | x => x
     end.

Type match 0, 1 return nat with
     | x, y => x + y
     end.

Type match 0, 1 with
     | x, y => x + y
     end.

Type match 0, 1 return nat with
     | O, y => y
     | S x, y => x + y
     end.

Type match 0, 1 with
     | O, y => y
     | S x, y => x + y
     end.

Type match 0, 1 return nat with
     | O, x => x
     | S y, O => y
     | x, y => x + y
     end.

Type match 0, 1 with
     | O, x => x + 0
     | S y, O => y + 0
     | x, y => x + y
     end.

Type
  match 0, 1 return nat with
  | O, x => x + 0
  | S y, O => y + 0
  | x, y => x + y
  end.

Type
  match 0, 1 return nat with
  | O, x => x
  | S x as b, S y => b + x + y
  | x, y => x + y
  end.

Type
  match 0, 1 with
  | O, x => x
  | S x as b, S y => b + x + y
  | x, y => x + y
  end.

Type
  (fun l : List nat =>
   match l return (List nat) with
   | Nil _ => Nil nat
   | Cons _ a l => l
   end).

Type (fun l : List nat => match l with
                          | Nil _ => Nil nat
                          | Cons _ a l => l
                          end).

Type match Nil nat return nat with
     | Nil _ => 0
     | Cons _ a l => S a
     end.
Type match Nil nat with
     | Nil _ => 0
     | Cons _ a l => S a
     end.

Type match Nil nat return (List nat) with
     | Cons _ a l => l
     | x => x
     end.

Type match Nil nat with
     | Cons _ a l => l
     | x => x
     end.

Type
  match Nil nat return (List nat) with
  | Nil _ => Nil nat
  | Cons _ a l => l
  end.

Type match Nil nat with
     | Nil _ => Nil nat
     | Cons _ a l => l
     end.

Type
  match 0 return nat with
  | O => 0
  | S x => match Nil nat return nat with
           | Nil _ => x
           | Cons _ a l => x + a
           end
  end.

Type
  match 0 with
  | O => 0
  | S x => match Nil nat with
           | Nil _ => x
           | Cons _ a l => x + a
           end
  end.

Type
  (fun y : nat =>
   match y with
   | O => 0
   | S x => match Nil nat with
            | Nil _ => x
            | Cons _ a l => x + a
            end
   end).

Type
  match 0, Nil nat return nat with
  | O, x => 0
  | S x, Nil _ => x
  | S x, Cons _ a l => x + a
  end.

Type
  (fun (n : nat) (l : listn n) =>
   match l return nat with
   | niln => 0
   | x => 0
   end).

Type (fun (n : nat) (l : listn n) => match l with
                                     | niln => 0
                                     | x => 0
                                     end).

Type match niln return nat with
     | niln => 0
     | x => 0
     end.

Type match niln with
     | niln => 0
     | x => 0
     end.

Type match niln return nat with
     | niln => 0
     | consn n a l => a
     end.
Type match niln with
     | niln => 0
     | consn n a l => a
     end.

Type
  match niln in (listn n) return nat with
  | consn m _ niln => m
  | _ => 1
  end.

Type
  (fun (n x : nat) (l : listn n) =>
   match x, l return nat with
   | O, niln => 0
   | y, x => 0
   end).

Type match 0, niln return nat with
     | O, niln => 0
     | y, x => 0
     end.

Type match niln, 0 return nat with
     | niln, O => 0
     | y, x => 0
     end.

Type match niln, 0 with
     | niln, O => 0
     | y, x => 0
     end.

Type match niln, niln return nat with
     | niln, niln => 0
     | x, y => 0
     end.

Type match niln, niln with
     | niln, niln => 0
     | x, y => 0
     end.

Type
  match niln, niln, niln return nat with
  | niln, niln, niln => 0
  | x, y, z => 0
  end.

Type match niln, niln, niln with
     | niln, niln, niln => 0
     | x, y, z => 0
     end.

Type match niln return nat with
     | niln => 0
     | consn n a l => 0
     end.

Type match niln with
     | niln => 0
     | consn n a l => 0
     end.

Type
  match niln, niln return nat with
  | niln, niln => 0
  | niln, consn n a l => n
  | consn n a l, x => a
  end.

Type
  match niln, niln with
  | niln, niln => 0
  | niln, consn n a l => n
  | consn n a l, x => a
  end.

Type
  (fun (n : nat) (l : listn n) =>
   match l return nat with
   | niln => 0
   | x => 0
   end).

Type
  (fun (c : nat) (s : bool) =>
   match c, s return nat with
   | O, _ => 0
   | _, _ => c
   end).

Type
  (fun (c : nat) (s : bool) =>
   match c, s return nat with
   | O, _ => 0
   | S _, _ => c
   end).

(* Rows of pattern variables: some tricky cases *)
Axioms (P : nat -> Prop) (f : forall n : nat, P n).

Type
  (fun i : nat =>
   match true, i as n return (P n) with
   | true, k => f k
   | _, k => f k
   end).

Type
  (fun i : nat =>
   match i as n, true return (P n) with
   | k, true => f k
   | k, _ => f k
   end).

(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
* it has to synthesize the predicate on O (which he can't)
*)
Type
  match 0 as n return match n with
                      | O => bool
                      | S _ => nat
                      end with
  | O => true
  | S _ => 0
  end.

Type (fun (n : nat) (l : listn n) => match l with
                                     | niln => 0
                                     | x => 0
                                     end).

Type
  (fun (n : nat) (l : listn n) =>
   match l return nat with
   | niln => 0
   | consn n a niln => 0
   | consn n a (consn m b l) => n + m
   end).

Type
  (fun (n : nat) (l : listn n) =>
   match l with
   | niln => 0
   | consn n a niln => 0
   | consn n a (consn m b l) => n + m
   end).

Type
  (fun (n : nat) (l : listn n) =>
   match l return nat with
   | niln => 0
   | consn n a niln => 0
   | consn n a (consn m b l) => n + m
   end).

Type
  (fun (n : nat) (l : listn n) =>
   match l with
   | niln => 0
   | consn n a niln => 0
   | consn n a (consn m b l) => n + m
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l return nat with
   | Niln _ => 0
   | Consn _ n a (Niln _) => 0
   | Consn _ n a (Consn _ m b l) => n + m
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l with
   | Niln _ => 0
   | Consn _ n a (Niln _) => 0
   | Consn _ n a (Consn _ m b l) => n + m
   end).

Type
  (fun (A:Set) (n:nat) (l:Listn A n) =>
    match l return Listn A O with
      | Niln _ as b => b
      | Consn _  n a (Niln _ as b) => (Niln A)
      | Consn _ n a (Consn _ m b l) => (Niln A)
    end).

(*
Type
  (fun (A:Set) (n:nat) (l:Listn A n) =>
    match l with
      | Niln _ as b => b
      | Consn _ n a (Niln _ as b) => (Niln A)
      | Consn _ n a (Consn _ m b l) => (Niln A)
    end).
*)

Type
  (fun (A:Set) (n:nat) (l:Listn A n) =>
    match l return Listn A (S 0) with
      | Niln _ as b => Consn A O O b
      | Consn _ n a (Niln _) as L => L
      | Consn _ n a _ => Consn A O O (Niln A)
    end).

Type
  (fun (A:Set) (n:nat) (l:Listn A n) =>
    match l return Listn A (S 0) with
      | Niln _ as b => Consn A O O b
      | Consn _ n a (Niln _) as L => L
      | Consn _ n a _ => Consn A O O (Niln A)
    end).

(* To test treatment of as-patterns in depth *)
Type
  (fun (A : Set) (l : List A) =>
   match l with
   | Nil _ as b => Nil A
   | Cons _ a (Nil _) as L => L
   | Cons _ a (Cons _ b m) as L => L
   end).

Type
  (fun (n : nat) (l : listn n) =>
   match l return (listn n) with
   | niln => l
   | consn n a c => l
   end).
Type
  (fun (n : nat) (l : listn n) =>
   match l with
   | niln => l
   | consn n a c => l
   end).

Type
  (fun (n : nat) (l : listn n) =>
   match l return (listn n) with
   | niln as b => l
   | _ => l
   end).

Type
  (fun (n : nat) (l : listn n) => match l with
                                  | niln as b => l
                                  | _ => l
                                  end).

Type
  (fun (n : nat) (l : listn n) =>
   match l return (listn n) with
   | niln as b => l
   | x => l
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l with
   | Niln _ as b => l
   | _ => l
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l return (Listn A n) with
   | Niln _ => l
   | Consn _ n a (Niln _) => l
   | Consn _ n a (Consn _ m b c) => l
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l with
   | Niln _ => l
   | Consn _ n a (Niln _) => l
   | Consn _ n a (Consn _ m b c) => l
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l return (Listn A n) with
   | Niln _ as b => l
   | Consn _ n a (Niln _ as b) => l
   | Consn _ n a (Consn _ m b _) => l
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l with
   | Niln _ as b => l
   | Consn _ n a (Niln _ as b) => l
   | Consn _ n a (Consn _ m b _) => l
   end).

Type
  match niln return nat with
  | niln => 0
  | consn n a niln => 0
  | consn n a (consn m b l) => n + m
  end.

Type
  match niln with
  | niln => 0
  | consn n a niln => 0
  | consn n a (consn m b l) => n + m
  end.

Type match LeO 0 return nat with
     | LeO x => x
     | LeS n m h => n + m
     end.

Type match LeO 0 with
     | LeO x => x
     | LeS n m h => n + m
     end.

Type
  (fun (n : nat) (l : Listn nat n) =>
   match l return nat with
   | Niln _ => 0
   | Consn _ n a l => 0
   end).

Type
  (fun (n : nat) (l : Listn nat n) =>
   match l with
   | Niln _ => 0
   | Consn _ n a l => 0
   end).

Type match Niln nat with
     | Niln _ => 0
     | Consn _ n a l => 0
     end.

Type match LE_n 0 return nat with
     | LE_n _ => 0
     | LE_S _ m h => 0
     end.

Type match LE_n 0 with
     | LE_n _ => 0
     | LE_S _ m h => 0
     end.

Type match LE_n 0 with
     | LE_n _ => 0
     | LE_S _ m h => 0
     end.

Type
  match niln return nat with
  | niln => 0
  | consn n a niln => n
  | consn n a (consn m b l) => n + m
  end.

Type
  match niln with
  | niln => 0
  | consn n a niln => n
  | consn n a (consn m b l) => n + m
  end.

Type
  match Niln nat return nat with
  | Niln _ => 0
  | Consn _ n a (Niln _
) => n
  | Consn _ n a (Consn _ m b l) => n + m
  end.

Type
  match Niln nat with
  | Niln _ => 0
  | Consn _ n a (Niln _) => n
  | Consn _ n a (Consn _ m b l) => n + m
  end.

Type
  match LeO 0 return nat with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => n + x
  end.

Type
  match LeO 0 with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => n + x
  end.

Type
  match LeO 0 return nat with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => m
  end.

Type
  match LeO 0 with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => m
  end.

Type
  (fun (n m : nat) (h : Le n m) =>
   match h return nat with
   | LeO x => x
   | x => 0
   end).

Type (fun (n m : nat) (h : Le n m) => match h with
                                      | LeO x => x
                                      | x => 0
                                      end).

Type
  (fun (n m : nat) (h : Le n m) =>
   match h return nat with
   | LeS n m h => n
   | x => 0
   end).

Type
  (fun (n m : nat) (h : Le n m) => match h with
                                   | LeS n m h => n
                                   | x => 0
                                   end).

Type
  (fun (n m : nat) (h : Le n m) =>
   match h return (nat * nat) with
   | LeO n => (0, n)
   | LeS n m _ => (S n, S m)
   end).

Type
  (fun (n m : nat) (h : Le n m) =>
   match h with
   | LeO n => (0, n)
   | LeS n m _ => (S n, S m)
   end).

Module Type F_v1.
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
  match h in (Le n m) return (Le n (S m)) with
  | LeO m' => LeO (S m')
  | LeS n' m' h' => LeS n' (S m') (F n' m' h')
  end.
End F_v1.

Module Type F_v2.
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
  match h in (Le n m) return (Le n (S m)) with
  | LeS n m h => LeS n (S m) (F n m h)
  | LeO m => LeO (S m)
  end.
End F_v2.

(* Rend la longueur de la liste *)

Module Type L1.
Definition length (n : nat) (l : listn n) :=
  match l return nat with
  | consn n _ (consn m _ _) => S (S m)
  | consn n _ _ => 1
  | _ => 0
  end.
End L1.

Module Type L1'.
Definition length (n : nat) (l : listn n) :=
  match l with
  | consn n _ (consn m _ _) => S (S m)
  | consn n _ _ => 1
  | _ => 0
  end.
End L1'.

Module Type L2.
Definition length (n : nat) (l : listn n) :=
  match l return nat with
  | consn n _ (consn m _ _) => S (S m)
  | consn n _ _ => S n
  | _ => 0
  end.
End L2.

Module Type L2'.
Definition length (n : nat) (l : listn n) :=
  match l with
  | consn n _ (consn m _ _) => S (S m)
  | consn n _ _ => S n
  | _ => 0
  end.
End L2'.

Module Type L3.
Definition length (n : nat) (l : listn n) :=
  match l return nat with
  | consn n _ (consn m _ l) => S n
  | consn n _ _ => 1
  | _ => 0
  end.
End L3.

Module Type L3'.
Definition length (n : nat) (l : listn n) :=
  match l with
  | consn n _ (consn m _ l) => S n
  | consn n _ _ => 1
  | _ => 0
  end.
End L3'.

Type match LeO 0 return nat with
     | LeS n m h => n + m
     | x => 0
     end.
Type match LeO 0 with
     | LeS n m h => n + m
     | x => 0
     end.

Type
  (fun (n m : nat) (h : Le n m) =>
   match h return nat with
   | LeO x => x
   | LeS n m (LeO x) => x + m
   | LeS n m (LeS x y h) => n + (m + (x + y))
   end).

Type
  (fun (n m : nat) (h : Le n m) =>
   match h with
   | LeO x => x
   | LeS n m (LeO x) => x + m
   | LeS n m (LeS x y h) => n + (m + (x + y))
   end).

Type
  match LeO 0 return nat with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => n + (m + (x + y))
  end.

Type
  match LeO 0 with
  | LeO x => x
  | LeS n m (LeO x) => x + m
  | LeS n m (LeS x y h) => n + (m + (x + y))
  end.

Type
  match LE_n 0 return nat with
  | LE_n _ => 0
  | LE_S _ m (LE_n _) => 0 + m
  | LE_S _ m (LE_S _ y h) => 0 + m
  end.

Type
  match LE_n 0 with
  | LE_n _ => 0
  | LE_S _ m (LE_n _) => 0 + m
  | LE_S _ m (LE_S _ y h) => 0 + m
  end.

Type (fun (n m : nat) (h : Le n m) => match h with
                                      | x => x
                                      end).

Type
  (fun (n m : nat) (h : Le n m) =>
   match h return nat with
   | LeO n => n
   | x => 0
   end).
Type (fun (n m : nat) (h : Le n m) => match h with
                                      | LeO n => n
                                      | x => 0
                                      end).

Type
  (fun n : nat =>
   match niln return (nat -> nat) with
   | niln => fun _ : nat => 0
   | consn n a niln => fun _ : nat => 0
   | consn n a (consn m b l) => fun _ : nat => n + m
   end).

Type
  (fun n : nat =>
   match niln with
   | niln => fun _ : nat => 0
   | consn n a niln => fun _ : nat => 0
   | consn n a (consn m b l) => fun _ : nat => n + m
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l return (nat -> nat) with
   | Niln _ => fun _ : nat => 0
   | Consn _ n a (Niln _) => fun _ : nat => n
   | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m
   end).

Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l with
   | Niln _ => fun _ : nat => 0
   | Consn _ n a (Niln _) => fun _ : nat => n
   | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m
   end).

(* Also tests for multiple _ patterns *)
Type
  (fun (A : Set) (n : nat) (l : Listn A n) =>
   match l in (Listn _ n) return (Listn A n) with
   | Niln _ as b => b
   | Consn _ _ _ _ as b => b
   end).

(** This one was said to raised once an "Horrible error message!" *)

Type
  (fun (A:Set) (n:nat) (l:Listn A n) =>
   match l with
   | Niln _ as b => b
   | Consn _ _ _ _  as b =>  b
   end).

Type
  match niln in (listn n) return (listn n) with
  | niln as b => b
  | consn _ _ _ as b => b
  end.

Type
  match niln in (listn n) return (listn n) with
  | niln as b => b
  | x => x
  end.

Type
  (fun (n m : nat) (h : LE n m) =>
   match h return (nat -> nat) with
   | LE_n _ => fun _ : nat => n
   | LE_S _ m (LE_n _) => fun _ : nat => n + m
   | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y
   end).
Type
  (fun (n m : nat) (h : LE n m) =>
   match h with
   | LE_n _ => fun _ : nat => n
   | LE_S _ m (LE_n _) => fun _ : nat => n + m
   | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y
   end).

Type
  (fun (n m : nat) (h : LE n m) =>
   match h return nat with
   | LE_n _ => n
   | LE_S _ m (LE_n _) => n + m
   | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y
   | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y')
   end).

Type
  (fun (n m : nat) (h : LE n m) =>
   match h with
   | LE_n _ => n
   | LE_S _ m (LE_n _) => n + m
   | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y
   | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y')
   end).

Type
  (fun (n m : nat) (h : LE n m) =>
   match h return nat with
   | LE_n _ => n
   | LE_S _ m (LE_n _) => n + m
   | LE_S _ m (LE_S _ y h) => n + m + y
   end).

Type
  (fun (n m : nat) (h : LE n m) =>
   match h with
   | LE_n _ => n
   | LE_S _ m (LE_n _) => n + m
   | LE_S _ m (LE_S _ y h) => n + m + y
   end).

Type
  (fun n m : nat =>
   match LeO 0 return nat with
   | LeS n m h => n + m
   | x => 0
   end).

Type (fun n m : nat => match LeO 0 with
                       | LeS n m h => n + m
                       | x => 0
                       end).

Parameter test : forall n : nat, {0 <= n} + {False}.
Type (fun n : nat => match test n return nat with
                     | left _ => 0
                     | _ => 0
                     end).

Type (fun n : nat => match test n return nat with
                     | left _ => 0
                     | _ => 0
                     end).

Type (fun n : nat => match test n with
                     | left _ => 0
                     | _ => 0
                     end).

Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
Type
  match compare 0 0 return nat with

      (* k<i *) | inleft (left _) => 0
   (* k=i *) | inleft _ => 0
   (* k>i *) | inright _ => 0
  end.

Type
  match compare 0 0 with

      (* k<i *) | inleft (left _) => 0
   (* k=i *) | inleft _ => 0
   (* k>i *) | inright _ => 0
  end.

CoInductive SStream (A : Set) : (nat -> A -> Prop) -> Type :=
    scons :
      forall (P : nat -> A -> Prop) (a : A),
      P 0 a -> SStream A (fun n : nat => P (S n)) -> SStream A P.
Parameter B : Set.

Type
  (fun (P : nat -> B -> Prop) (x : SStream B P) =>
   match x return B with
   | scons _ _ a _ _ => a
   end).

Type
  (fun (P : nat -> B -> Prop) (x : SStream B P) =>
   match x with
   | scons _ _ a _ _ => a
   end).

Type match (0, 0) return (nat * nat) with
     | (x, y) => (S x, S y)
     end.
Type match (0, 0) return (nat * nat) with
     | (b, y) => (S b, S y)
     end.
Type match (0, 0) return (nat * nat) with
     | (x, y) => (S x, S y)
     end.

Type match (0, 0) with
     | (x, y) => (S x, S y)
     end.
Type match (0, 0) with
     | (b, y) => (S b, S y)
     end.
Type match (0, 0) with
     | (x, y) => (S x, S y)
     end.

Module Type test_concat.

Parameter concat : forall A : Set, List A -> List A -> List A.

Type
  match Nil nat, Nil nat return (List nat) with
  | Nil _ as b, x => concat nat b x
  | Cons _ _ _ as d, Nil _ as c => concat nat d c
  | _, _ => Nil nat
  end.
Type
  match Nil nat, Nil nat with
  | Nil _ as b, x => concat nat b x
  | Cons _ _ _ as d, Nil _ as c => concat nat d c
  | _, _ => Nil nat
  end.

End test_concat.

Inductive redexes : Set :=
  | VAR : nat -> redexes
  | Fun : redexes -> redexes
  | Ap : bool -> redexes -> redexes -> redexes.

Fixpoint regular (U : redexes) : Prop :=
  match U return Prop with
  | VAR n => True
  | Fun V => regular V
  | Ap true (Fun _ as V) W => regular V /\ regular W
  | Ap true _ W => False
  | Ap false V W => regular V /\ regular W
  end.

Type (fun n : nat => match n with
                     | O => 0
                     | S (S n as V) => V
                     | _ => 0
                     end).

Parameter
  concat :
    forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m).
Type
  (fun (n : nat) (l : listn n) (m : nat) (l' : listn m) =>
   match l in (listn n), l' return (listn (n + m)) with
   | niln, x => x
   | consn n a l'', x => consn (n + m) a (concat n l'' m x)
   end).

Type
  (fun (x y z : nat) (H : x = y) (H0 : y = z) =>
   match H return (x = z) with
   | refl_equal =>
       match H0 in (_ = n) return (x = n) with
       | refl_equal => H
       end
   end).

Type (fun h : False => match h return False with
                       end).

Type (fun h : False => match h return True with
                       end).

Definition is_zero (n : nat) := match n with
                                | O => True
                                | _ => False
                                end.

Type
  (fun (n : nat) (h : 0 = S n) =>
   match h in (_ = n) return (is_zero n) with
   | refl_equal => I
   end).

Definition disc (n : nat) (h : 0 = S n) : False :=
  match h in (_ = n) return (is_zero n) with
  | refl_equal => I
  end.

Definition nlength3 (n : nat) (l : listn n) :=
  match l with
  | niln => 0
  | consn O _ _ => 1
  | consn (S n) _ _ => S (S n)
  end.

(* == Testing strategy elimintation predicate  synthesis == *)
Section titi.
Variable h : False.
Type match 0 with
     | O => 0
     | _ => except h
     end.
End titi.

Type match niln with
     | consn _ a niln => a
     | consn n _ x => 0
     | niln => 0
     end.

Inductive wsort : Set :=
  | ws : wsort
  | wt : wsort.
Inductive TS : wsort -> Set :=
  | id : TS ws
  | lift : TS ws -> TS ws.

Type
  (fun (b : wsort) (M N : TS b) =>
   match M, N with
   | lift M1, id => False
   | _, _ => True
   end).

(* ===================================================================== *)
(* To test pattern matching over a non-dependent inductive type, but     *)
(* having constructors with some arguments that depend on others         *)
(* I.e. to test manipulation of elimination predicate                    *)
(* ===================================================================== *)

Module Type test_term.

Parameter LTERM : nat -> Set.
Inductive TERM : Type :=
  | var : TERM
  | oper : forall op : nat, LTERM op -> TERM.

Parameter t1 t2 : TERM.

Type
  match t1, t2 with
  | var, var => True
  | oper op1 l1, oper op2 l2 => False
  | _, _ => False
  end.

End test_term.

Require Import Peano_dec.
Parameter n : nat.
Definition eq_prf := exists m : _, n = m.
Parameter p : eq_prf.

Type
  match p with
  | ex_intro _ c eqc =>
      match eq_nat_dec c n with
      | right _ => refl_equal n
      | left y => (* c=n*)  refl_equal n
      end
  end.

Parameter ordre_total : nat -> nat -> Prop.

Parameter N_cla : forall N : nat, {N = 0} + {N = 1} + {N >= 2}.

Parameter
  exist_U2 :
    forall N : nat,
    N >= 2 ->
    {n : nat |
    forall m : nat, 0 < m /\ m <= N /\ ordre_total n m /\ 0 < n /\ n < N}.

Type
  (fun N : nat =>
   match N_cla N with
   | inright H => match exist_U2 N H with
                  | exist _ a b => a
                  end
   | _ => 0
   end).

(* ============================================== *)
(*     To test compilation of dependent case      *)
(*  Nested patterns                               *)
(* ============================================== *)

(* == To test that terms named with AS are correctly absolutized before
      substitution in rhs   == *)

Type
  (fun n : nat =>
   match n return nat with
   | O => 0
   | S O => 0
   | S (S n1) as N => N
   end).

(* ========= *)

Type
  match niln in (listn n) return Prop with
  | niln => True
  | consn (S O) _ _ => False
  | _ => True
  end.

Type
  match niln in (listn n) return Prop with
  | niln => True
  | consn (S (S O)) _ _ => False
  | _ => True
  end.

Type
  match LeO 0 as h in (Le n m) return nat with
  | LeO _ => 0
  | LeS (S x) _ _ => x
  | _ => 1
  end.

Type
  match LeO 0 as h in (Le n m) return nat with
  | LeO _ => 0
  | LeS (S x) (S y) _ => x
  | _ => 1
  end.

Type
  match LeO 0 as h in (Le n m) return nat with
  | LeO _ => 0
  | LeS (S x as b) (S y) _ => b
  | _ => 1
  end.

Module Type ff.

Parameter ff : forall n m : nat, n <> m -> S n <> S m.
Parameter discr_r : forall n : nat, 0 <> S n.
Parameter discr_l : forall n : nat, S n <> 0.

Type
  (fun n : nat =>
   match n return (n = 0 \/ n <> 0) with
   | O => or_introl (0 <> 0) (refl_equal 0)
   | S x => or_intror (S x = 0) (discr_l x)
   end).

Module Type eqdec.

Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
  match n, m return (n = m \/ n <> m) with
  | O, O => or_introl (0 <> 0) (refl_equal 0)
  | O, S x => or_intror (0 = S x) (discr_r x)
  | S x, O => or_intror _ (discr_l x)
  | S x, S y =>
      match eqdec x y return (S x = S y \/ S x <> S y) with
      | or_introl h => or_introl (S x <> S y) (f_equal S h)
      | or_intror h => or_intror (S x = S y) (ff x y h)
      end
  end.

End eqdec.

Module Type eqdec'.

Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
  match n return (forall m : nat, n = m \/ n <> m) with
  | O =>
      fun m : nat =>
      match m return (0 = m \/ 0 <> m) with
      | O => or_introl (0 <> 0) (refl_equal 0)
      | S x => or_intror (0 = S x) (discr_r x)
      end
  | S x =>
      fun m : nat =>
      match m return (S x = m \/ S x <> m) with
      | O => or_intror (S x = 0) (discr_l x)
      | S y =>
          match eqdec x y return (S x = S y \/ S x <> S y) with
          | or_introl h => or_introl (S x <> S y) (f_equal S h)
          | or_intror h => or_intror (S x = S y) (ff x y h)
          end
      end
  end.

End eqdec'.

Inductive empty : forall n : nat, listn n -> Prop :=
    intro_empty : empty 0 niln.

Parameter
  inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).

Type
  (fun (n : nat) (l : listn n) =>
   match l in (listn n) return (empty n l \/ ~ empty n l) with
   | niln => or_introl (~ empty 0 niln) intro_empty
   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
   end).

End ff.

Module Type ff'.

Parameter ff : forall n m : nat, n <> m -> S n <> S m.
Parameter discr_r : forall n : nat, 0 <> S n.
Parameter discr_l : forall n : nat, S n <> 0.

Type
  (fun n : nat =>
   match n return (n = 0 \/ n <> 0) with
   | O => or_introl (0 <> 0) (refl_equal 0)
   | S x => or_intror (S x = 0) (discr_l x)
   end).

Module Type eqdec.

Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
  match n, m return (n = m \/ n <> m) with
  | O, O => or_introl (0 <> 0) (refl_equal 0)
  | O, S x => or_intror (0 = S x) (discr_r x)
  | S x, O => or_intror _ (discr_l x)
  | S x, S y =>
      match eqdec x y return (S x = S y \/ S x <> S y) with
      | or_introl h => or_introl (S x <> S y) (f_equal S h)
      | or_intror h => or_intror (S x = S y) (ff x y h)
      end
  end.

End eqdec.

Module Type eqdec'.

Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
  match n return (forall m : nat, n = m \/ n <> m) with
  | O =>
      fun m : nat =>
      match m return (0 = m \/ 0 <> m) with
      | O => or_introl (0 <> 0) (refl_equal 0)
      | S x => or_intror (0 = S x) (discr_r x)
      end
  | S x =>
      fun m : nat =>
      match m return (S x = m \/ S x <> m) with
      | O => or_intror (S x = 0) (discr_l x)
      | S y =>
          match eqdec x y return (S x = S y \/ S x <> S y) with
          | or_introl h => or_introl (S x <> S y) (f_equal S h)
          | or_intror h => or_intror (S x = S y) (ff x y h)
          end
      end
  end.

End eqdec'.
End ff'.

(* ================================================== *)
(* Pour tester parametres                             *)
(* ================================================== *)

Inductive Empty (A : Set) : List A -> Prop :=
    intro_Empty : Empty A (Nil A).

Parameter
  inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).

Type
  match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with
  | Nil _ => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat)
  | Cons _ a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y)
  end.

(* ================================================== *)
(* Sur les listes                                     *)
(* ================================================== *)

Inductive empty : forall n : nat, listn n -> Prop :=
    intro_empty : empty 0 niln.

Parameter
  inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).

Type
  (fun (n : nat) (l : listn n) =>
   match l in (listn n) return (empty n l \/ ~ empty n l) with
   | niln => or_introl (~ empty 0 niln) intro_empty
   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
   end).

(* ===================================== *)
(*   Test parametros:                    *)
(* ===================================== *)

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).

Type
  match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
  | Nil _, Nil _ => V1
  | Nil _, Cons _ a x => V2 a x
  | Cons _ a x, Nil _ => V3 a x
  | Cons _ a x, Cons _ b y => V4 a x b y
  end.

Type
  (fun x y : List nat =>
   match x, y return (eqlong x y \/ ~ eqlong x y) with
   | Nil _, Nil _ => V1
   | Nil _, Cons _ a x => V2 a x
   | Cons _ a x, Nil _ => V3 a x
   | Cons _ a x, Cons _ b y => V4 a x b y
   end).

(* ===================================== *)

Inductive Eqlong :
forall n : nat, listn n -> forall m : nat, listn m -> Prop :=
  | Eql_cons :
      forall (n m : nat) (x : listn n) (y : listn m) (a b : nat),
      Eqlong n x m y -> Eqlong (S n) (consn n a x) (S m) (consn m b y)
  | Eql_niln : Eqlong 0 niln 0 niln.

Parameter W1 : Eqlong 0 niln 0 niln \/ ~ Eqlong 0 niln 0 niln.
Parameter
  W2 :
    forall (n a : nat) (x : listn n),
    Eqlong 0 niln (S n) (consn n a x) \/ ~ Eqlong 0 niln (S n) (consn n a x).
Parameter
  W3 :
    forall (n a : nat) (x : listn n),
    Eqlong (S n) (consn n a x) 0 niln \/ ~ Eqlong (S n) (consn n a x) 0 niln.
Parameter
  W4 :
    forall (n a : nat) (x : listn n) (m b : nat) (y : listn m),
    Eqlong (S n) (consn n a x) (S m) (consn m b y) \/
    ~ Eqlong (S n) (consn n a x) (S m) (consn m b y).

Type
  match
    niln as x in (listn n), niln as y in (listn m)
    return (Eqlong n x m y \/ ~ Eqlong n x m y)
  with
  | niln, niln => W1
  | niln, consn n a x => W2 n a x
  | consn n a x, niln => W3 n a x
  | consn n a x, consn m b y => W4 n a x m b y
  end.

Type
  (fun (n m : nat) (x : listn n) (y : listn m) =>
   match
     x in (listn n), y in (listn m)
     return (Eqlong n x m y \/ ~ Eqlong n x m y)
   with
   | niln, niln => W1
   | niln, consn n a x => W2 n a x
   | consn n a x, niln => W3 n a x
   | consn n a x, consn m b y => W4 n a x m b y
   end).

Parameter
  Inv_r :
    forall (n a : nat) (x : listn n), ~ Eqlong 0 niln (S n) (consn n a x).
Parameter
  Inv_l :
    forall (n a : nat) (x : listn n), ~ Eqlong (S n) (consn n a x) 0 niln.
Parameter
  Nff :
    forall (n a : nat) (x : listn n) (m b : nat) (y : listn m),
    ~ Eqlong n x m y -> ~ Eqlong (S n) (consn n a x) (S m) (consn m b y).

Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat)
(y : listn m) {struct x} : Eqlong n x m y \/ ~ Eqlong n x m y :=
  match
    x in (listn n), y in (listn m)
    return (Eqlong n x m y \/ ~ Eqlong n x m y)
  with
  | niln, niln => or_introl (~ Eqlong 0 niln 0 niln) Eql_niln
  | niln, consn n a x as L => or_intror (Eqlong 0 niln (S n) L) (Inv_r n a x)
  | consn n a x as L, niln => or_intror (Eqlong (S n) L 0 niln) (Inv_l n a x)
  | consn n a x as L1, consn m b y as L2 =>
      match
        Eqlongdec n x m y
        return (Eqlong (S n) L1 (S m) L2 \/ ~ Eqlong (S n) L1 (S m) L2)
      with
      | or_introl h =>
          or_introl (~ Eqlong (S n) L1 (S m) L2) (Eql_cons n m x y a b h)
      | or_intror h =>
          or_intror (Eqlong (S n) L1 (S m) L2) (Nff n a x m b y h)
      end
  end.

(* ============================================== *)
(*     To test compilation of dependent case      *)
(*      Multiple Patterns                         *)
(* ============================================== *)
Inductive skel : Type :=
  | PROP : skel
  | PROD : skel -> skel -> skel.

Parameter Can : skel -> Type.
Parameter default_can : forall s : skel, Can s.

Type
  (fun s1 s2 s1 s2 : skel =>
   match s1, s2 return (Can s1) with
   | PROP, PROP => default_can PROP
   | PROD x y, PROP => default_can (PROD x y)
   | PROD x y, _ => default_can (PROD x y)
   | PROP, _ => default_can PROP
   end).

(* to test bindings in nested Cases *)
(* ================================ *)
Inductive Pair : Set :=
  | pnil : Pair
  | pcons : Pair -> Pair -> Pair.

Type
  (fun p q : Pair =>
   match p with
   | pcons _ x => match q with
                  | pcons _ (pcons _ x) => True
                  | _ => False
                  end
   | _ => False
   end).

Type
  (fun p q : Pair =>
   match p with
   | pcons _ x =>
       match q with
       | pcons _ (pcons _ x) =>
           match q with
           | pcons _ (pcons _ (pcons _ x)) => x
           | _ => pnil
           end
       | _ => pnil
       end
   | _ => pnil
   end).

Type
  (fun (n : nat) (l : listn (S n)) =>
   match l in (listn z) return (listn (pred z)) with
   | niln => niln
   | consn n _ l =>
       match l in (listn m) return (listn m) with
       | niln => niln
       | b => b
       end
   end).

(* Test de la syntaxe avec nombres *)
Require Import Arith.
Type (fun n => match n with
               | S (S O) => true
               | _ => false
               end).

Require Import ZArith.
Type (fun n => match n with
               | Z0 => true
               | _ => false
               end).

(* Check that types with unknown sort, as A below, are not fatal to
   the pattern-matching compilation *)

Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
  match p with eq_refl => u end.

(* Check in-pattern clauses with constant constructors, which were
   previously interpreted as variables (before 8.5) *)

Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.

Check match niln in listn O return O=O with niln => eq_refl end.

(* A test about nested "as" clauses *)
(* (was failing up to May 2017) *)

Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.

(* A test about binding variables of "in" clause of "match" *)
(* (was failing from 8.5 to Dec 2018) *)

Check match O in nat return nat with O => O | _ => O end.

(* Checking that aliases are substituted in the correct order *)

Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.

¤ Dauer der Verarbeitung: 0.81 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.