Search code examples
coq

Dependent pattern match asks for a wildcard instead of proper type

Note: this code is similar (but not identical) to the code in Some help proving coq function terminates. Where that code deals with the question of equality, this tries to extend addition in this little language to include pairs.

Inductive type : Set :=
| Nat
| Bool
| Pair : type -> type -> type.

Inductive numeric: type -> Set :=
| NNat: numeric Nat
| MPair: forall a1 a2, numeric a1 -> numeric a2 -> numeric (Pair a1 a2).

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : forall t, numeric t -> tbinop t t t
| TTimes : forall t, numeric t -> tbinop t t t
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool
| TPair : forall in1 in2, tbinop in1 in2 (Pair in1 in2).

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Fixpoint typeDenote (t : type) : Set :=
  match t with
    | Nat => nat
    | Bool => bool
    | Pair l r => prod (typeDenote l) (typeDenote r)
  end.

Fixpoint typeDepth (t: type): nat :=
  match t with
  | Nat => 1
  | Bool => 1
  | Pair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
  end.

Program Fixpoint tbinopDepth arg1 arg2 res (b: tbinop arg1 arg2 res)
{measure (Nat.max (typeDepth arg1) (typeDepth arg2))}
  : nat :=
match b with
| TPlus _ => 1
| TTimes _ => 1
| TEq Nat => 1
| TEq Bool => 1
| TEq (Pair A B) => tbinopDepth (TPair A B)
| TLt => 1
| TPair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
end.
Next Obligation.
simpl.
rewrite Nat.max_idempotent.
omega.
Qed.

Eval compute in tbinopDepth (TEq (Pair Nat Nat)). (* 2 *)
Eval compute in tbinopDepth (TEq Nat). (* 1 *)

Program Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  {measure (tbinopDepth b)} : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
    | TPlus MNat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat
    | TPlus (MPair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (x1 + y1, x2 + y2)
        end : typeDenote (Pair A B)
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TEq (Pair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        false (* obviously extremely wrong, doing this to unlock pending https://stackoverflow.com/questions/62912587/some-help-proving-coq-function-terminates *)
        (*match a, b with
        | (x1, x2), (y1, y2) => eqb (tbinopDenote (TEq A) x1 y1) (tbinopDenote (TEq B) x2 y2)
        end : typeDenote Bool*)
    | TLt => leb
    | TPair _ _ => fun a b => (a,b)
  end.

when I try to compile this, I get the error

Found type "typeDenote Nat" where "typeDenote wildcard'" was expected.

My guess is that I need some way to connect typeDenote Nat to TPlus MNat. I have no clue. I am going to keep searching for information on Coq's dependent pattern matching. Would appreciate any pointers on how to achieve this sort of thing, as inductive types constrained on other inductive types seem pretty common in proofs!

Edit: I should add that my naive thought was that the match should look like this:

| TPlus Nat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat

but then it says: Found a constructor of inductive type type while a constructor of numeric is expected.. So I guess it automatically sort of narrows things downs and does the substituting, but I don't know how to connect it back to Nat to get it to typecheck.

Edit2: So, reading docs, playing around, I've arrived at this:

Program Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  {measure (tbinopDepth b)} : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b in tbinop arg1 arg2 res return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with
    | @TPlus Nat MNat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat
    | @TPlus (Pair A B) (MPair A' B') => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (tbinopDenote (@TPlus A A') x1 y1, tbinopDenote (@TPlus B B') x2 y2)
        end : typeDenote (Pair A B)
    | @TPlus _ _ => !
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TEq (Pair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        false (* obviously extremely wrong, doing this to unlock pending https://stackoverflow.com/questions/62912587/some-help-proving-coq-function-terminates *)
        (*match a, b with
        | (x1, x2), (y1, y2) => eqb (tbinopDenote (TEq A) x1 y1) (tbinopDenote (TEq B) x2 y2)
        end : typeDenote Bool*)
    | TLt => leb
    | TPair _ _ => fun a b => (a,b)
  end.

Compiling, I get the following error:

The term "x1" has type
 "(fix typeDenote (t : type) : Set :=
     match t with
     | Nat => nat
     | Bool => bool
     | Pair l r => (typeDenote l * typeDenote r)%type
     end) A" while it is expected to have type
 "tbinopDepth
    (TPlus (eq_rect t0 (fun H : type => numeric H) A' A ?e@{b0:=b; b:=b0})) <
  tbinopDepth b".

Which is the recursion error from the other question, rather than a typing one.

That said...is this the proper way to achieve this? I know Coq provides lots of ways to shoot ourselves in our feet :D

Another question:

| @TPlus (Pair A B) (MPair A' B') => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (tbinopDenote (@TPlus A A') x1 y1, tbinopDenote (@TPlus B B') x2 y2)
        end : typeDenote (Pair A B)

If this is indeed the correct way to do it, is there a way to prove that A=A' and B=B'? Is it necessary?

Solution

  • It is the same trick as in the question you mentioned: simply define the numeric operations separately:

    Require Import Coq.Arith.Arith.
Set Implicit Arguments.

Inductive type : Type :=
| Nat
| Bool
| Pair : type -> type -> type.

Inductive numeric: type -> Set :=
| NNat: numeric Nat
| MPair: forall a1 a2, numeric a1 -> numeric a2 -> numeric (Pair a1 a2).

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : forall t, numeric t -> tbinop t t t
| TTimes : tbinop Nat Nat Nat
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool
| TPair : forall in1 in2, tbinop in1 in2 (Pair in1 in2).

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Fixpoint typeDenote (t : type) : Type :=
  match t with
    | Nat => nat
    | Bool => bool
    | Pair l r => prod (typeDenote l) (typeDenote r)
  end.

Fixpoint typeDepth (t: type): nat :=
  match t with
  | Nat => 1
  | Bool => 1
  | Pair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
  end.

Fixpoint add t (n : numeric t) : typeDenote t -> typeDenote t -> typeDenote t :=
  match n in (numeric t0) return (typeDenote t0 -> typeDenote t0 -> typeDenote t0) with
  | NNat => Nat.add
  | @MPair a1 a2 n0 n1 => fun '(x1, y1) '(x2, y2) => (add n0 x1 x2, add n1 y1 y2)
  end.

Fixpoint eqb arg : typeDenote arg -> typeDenote arg -> bool :=
  match arg return typeDenote arg -> typeDenote arg -> bool with
  | Nat => Nat.eqb
  | Bool => Bool.eqb
  | Pair A B => fun '(x1, y1) '(x2, y2) => andb (eqb _ x1 x2) (eqb _ y1 y2)
  end.

Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res) {struct arg1}
    : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b in tbinop arg1 arg2 res return typeDenote arg1 -> typeDenote arg2 -> typeDenote res with
  | TPlus n => add n
  | TTimes => Nat.mul
  | TEq arg => eqb arg
  | TLt => leb
  | TPair _ _ => fun a b => (a,b)
  end.