Stream: Coq users

Topic: A dependent match issue


view this post on Zulip Pierre Rousselin (Aug 20 2023 at 09:04):

I tried to answer this SE question in a direct way and failed. I want to understand why.

Here is the context:

Fixpoint F (n: nat): Set :=
  match n with
  | 0 => bool
  | S n' => bool -> (F n')
  end.

Fixpoint B (n: nat): Set :=
  match n with
  | 0 => bool
  | 1 => bool
  | S n' => bool * (B n')
  end.

The user then wants to define recursively a function apply_fgiving the result of applying an n-ary function f to an n-tuple x. Here is my try:

Fixpoint apply_f {n: nat} : F n -> B n -> bool :=
  match n return F n -> B n -> bool with
    0 => fun f _ => f
  | S n' => match n' return F (S n') -> B (S n') -> bool with
              0 => fun f x => (f x)
            | S p => fun f x =>
                  (@apply_f n' (f (fst x)) (snd x))
            end
  end.

It fails with this error message:

In environment
apply_f : forall n : nat, F n -> B n -> bool
n : nat
n' : nat
p : nat
f : F (S (S p))
x : B (S (S p))
The term "f (fst x)" has type
 "bool ->
  (fix F (n : nat) : Set :=
     match n with
     | 0 => bool
     | S n' => bool -> F n'
     end) p" while it is expected to have type "F n'".

indicating that somehow, Coq does not in this context recognize that bool -> F p is convertible to F n'.
I would like to understand why and how it can be solved.
I tried to read the reference manual, but I don't understand this section, I don't know what an "elimination predicate" is and what is its purpose.

view this post on Zulip Karl Palmskog (Aug 20 2023 at 09:07):

probably not helpful in this case (if low-level understanding is the goal), but the standard answer to most dependent matching problems: switch to using Equations

view this post on Zulip Pierre Rousselin (Aug 20 2023 at 09:09):

Thanks for pointing it out, but I still feel I need to understand completely what happens with match. After all, it is the only primitive construct in Coq. (But trying Equations at some point is on my todo list).

view this post on Zulip Karl Palmskog (Aug 20 2023 at 10:04):

the Equations example here looks relevant: https://github.com/mattam82/Coq-Equations/blob/main/examples/MoreDep.v#L44-L139

if I was going to teach Coq, I'd probably have students use Equations instead of Fixpoint everywhere, and then writing the matches/Fixpoint manually would be a form of advanced exercises....

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:12):

I think you should pass S p to f, not n', for this to pass typechecking.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:14):

but I'm not sure that will pass guard-checking — I'm only talking about the typechecking part.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:14):

I was puzzled because you've already used the convoy pattern and written the return annotation I'd expect here.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:16):

To see why, you should be able to use refine to see the type of the match branch: matching n' against S p will replace n' by S p in the goal, but it will not remember that n' := S p, since that's not possible when the scrutinee is an expression.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:16):

one could record a propositional equality, but you must do that by hand.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:18):

Therefore, Coq is NOT allowed to consider n' and S p convertible, and that's why the typechecker demands S p here.

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 13:21):

That's also a general problem: AFAIK, Coq primitive pattern matching, like the destruct expr or case: expr tactics, will never remember that the scrutinee is equal to the match pattern. (Destruct has extra smarts, but not ones relevant in this scenario; case: avoids those). For that you need destruct expr eqn:?., or the generated proof term, which uses propositional equality.

view this post on Zulip Karl Palmskog (Aug 20 2023 at 13:29):

I guess Program Fixpoint might help with remembering scrutinee equality?

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 16:54):

“yes”, but “with friends like that who needs enemies” comes to mind, given the quadratic blowup to term size this can cause

view this post on Zulip Paolo Giarrusso (Aug 20 2023 at 16:58):

My perspective might be biased because of extra circumstances that made this pretty painful, but let’s just say Equations’ design makes two important changes: this behavior is opt-in, and Equations proves unfolding lemmas to hide the generated proof term :-).

view this post on Zulip Pierre Rousselin (Aug 21 2023 at 08:16):

Here is where I am at the moment. I still do not understand everything but it's getting better.
As @Paolo Giarrusso suggested, I tried using refine and destruct with an equation to build the function in proof mode.

Fixpoint apply_f {n: nat} : F n -> B n -> bool.
  Proof.
    refine
      match n return F n -> B n -> bool with
        0 => fun f _ => f
      | S n' => _
      end.
    destruct n' as [| p] eqn:E.
    - exact (fun f x => (f x)).
    - intros f x.
      rewrite <-E in f.
      refine (apply_f n' (f (fst x)) _).
      rewrite E. exact (snd x).
  Defined.

This works and is accepted. Inspecting the proof term and a lot of cleaning now gives:

Fixpoint apply_f2 {n : nat} : F n -> B n -> bool :=
  match n return (F n -> B n -> bool) with
  | 0 => fun f _ => f
  | S n' =>
      match n' as k return (k = n' -> F (S k) -> B (S k) -> bool) with
      | 0 => fun _ f x => f x
      | S p =>
          (fun E f x =>
           apply_f2 ((eq_rec _ (fun i => F (S i)) f _ E) (fst x))
             (eq_rec (S p) B (snd x) _ E))
      end (eq_refl n')
  end.

For clarity, here is the definition of eq_rec (well, of eq_rect but it is the same):

eq_rect =
fun (A : Type) (x : A) (P : A -> Type) (f : P x) (a : A) (e : x = a) =>
match e in (_ = a0) return (P a0) with
| eq_refl => f
end
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall a : A, x = a -> P a

Arguments eq_rect [A]%type_scope x P%function_scope f y e
  (where some original arguments have been renamed)

Last updated: Jun 13 2024 at 21:01 UTC