0
$\begingroup$

In Coq, While trying to write a definition of a function with well-founded recursion, I found myself wanting/having to reference that a term I was trying to match hdtl l had been destructed into a particular pattern (Some ..., ...) as seen in the (bogus/incorrect/failing) definition of foo. How can we access such facts/terms? (I am asking for a way/method to get these types)

For more context, foo is not structurally recursive, and I want to instead define it with well founded recursion (cf Leroy). The proof obligation generated by function uses the fact that (Some ..., ...) = hdtl l. The end goal is to eliminate the use of Program when defining foo, which requires being able to replace the hole with an explicit term.


Definition hdtl (lst: list nat) :=
  match lst with
  h :: t => (Some h, t)
  | _    => (None, [])
  end.

Fail Fixpoint foo acc l :=
  match hdtl l with
  | (Some h, t) => foo (h :: acc) t
  | (None  , _) => acc
  end.

(* Program Fixpoint foo acc l (ACC: Acc lt (length l)) {struct ACC} :=
  match hdtl l with
  | (Some h, t) => foo (h :: acc) t (Acc_inv ACC _) (* <-- hole used to generate foo_oblig's type *)
  | (None  , _) => acc
  end.

Next Obligation. *)

Remark foo_oblig : forall l h t (ACC : Acc lt (length l)),
  (Some h, t) = hdtl l -> length t < length l.
Proof. unfold hdtl.
   intros [|h' t'] * ?;
   [ inversion 1
   | injection 1 as <- <-; left ].
Qed.


Program Fixpoint foo acc l (ACC: Acc lt (length l)) {struct ACC} :=
  match hdtl l with
  | (Some h, t) => foo (h :: acc) t (Acc_inv ACC (foo_oblig l h t ACC _)) (* <-- what type? *)
  | (None  , _) => acc
  end.
$\endgroup$
5
  • 1
    $\begingroup$ I didn't understand the question: the Program Fixpoint foo you commented generates an obligation that is trivial because you have the assumption Heq_anonymous : (Some h, t) = hdtl l. Why are you not satisfied with it and are you trying to write another (more complicated) Program Fixpoint foo? $\endgroup$
    – Bruno
    Jan 27 at 4:09
  • $\begingroup$ 1) I want to eliminate the use of Program in the defn of foo. 2) I want to learn how to access terms of type (Some h, t) = hdtl l The real main purpose is due to the belief that these (1 & 2) will help with edification/learning. The current unfold term representing foo is quite unreadable $\endgroup$
    – C.E.Sally
    Jan 27 at 4:16
  • $\begingroup$ Also, I can't work with the function produced by Program (in particular, I can't get the match statement to reduce $\endgroup$
    – C.E.Sally
    Jan 27 at 5:53
  • $\begingroup$ You should just have a look at the term produced by Program Fixpoint. It makes use of the convoy pattern (bringing a proof of equality around to remember) which is also what you need to do by hand. It is a nice exercise to do, but the canonical way to do it nowadays is to use the Equation plugin and use its fixpoint equality (automatically generated) to rewrite instead of computing with the function. Unless you really need to compute with it (ie you want it to appear in a dependent type or use it in a reflexive tactic). $\endgroup$ Jan 27 at 11:02
  • $\begingroup$ Thanks for the pointer; I will check that out. $\endgroup$
    – C.E.Sally
    Jan 31 at 7:55

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.