Justin Kelm (Mar 22 2024 at 06:23): Justin Kelm (Mar 22 2024 at 06:23):For more complex programs, I often run into the problem mentioned here, where I need to deduce extra information from the result of a match: https://stackoverflow.com/questions/27316254/coq-keeping-information-in-a-match-statement
That approach works well, until I need to manipulate those definitions in later proofs. Here's an example:
Parameter foo : nat -> list nat.
Parameter bar : forall n, foo n <> nil -> nat.
(* Want baz to equal 42 when foo returns nil, and otherwise to equal bar. *)
Definition baz (n : nat) : nat.
refine (match foo n with
| nil => 42
| cons m ls => _ end).
(* We have no info about foo n... *)
Abort.
I employ the trick in the above link:
Definition baz (n : nat) : nat.
refine (match foo n as x return foo n = x -> nat with
| nil => fun _ => 42
| _ => _ end eq_refl).
intro; apply (bar n); congruence. Defined.
But let's say I want to prove something:
Axiom bar_fact : forall n H, bar n H <> 0.
Theorem baz_fact : forall n, baz n <> 0.
Proof. intros; unfold baz. destruct (foo n).
(* ERROR: Abstracting over the term "l" leads to a term ... which is ill-typed. *)
There appear to be a number of threads on this:
https://stackoverflow.com/questions/14867685/abstracting-leads-to-a-term-ill-typed-yet-well-typed?rq=3
https://stackoverflow.com/questions/63027162/abstraction-typing-error-resulting-from-case-eq-and-rewriting-in-coq
https://stackoverflow.com/questions/59223096/abstracting-over-the-terms-is-ill-defined-when-destructuring
but only the second presents what I regard as a generally applicable workaround to Coq's gaucheness with match terms. Indeed, importing ssreflect and continuing with generalize (eq_refl (foo n)); case: {2 3}(foo n) allows the proof of baz_fact to be completed.
My question is, are there any alternative ways to define baz and/or prove baz_fact, especially within base Coq? This seems to be something of an unnatural solution to a problem that arises naturally among beginners.
In this particular instance, it would be straightforward to rewrite baz with an if-then using a sumbool type:
Definition is_nil : forall ls : list nat, { ls = nil } + { ls <> nil }.
Proof. now destruct ls; left+right. Qed.
Definition baz (n : nat) : nat.
refine (if is_nil (foo n) then 42 else _). now apply (bar n). Defined.
(* baz =
fun n : nat =>
match is_nil (foo n) with
| left _ => 42
| right x => bar n x
end
: nat -> nat *)
and destruct is much better behaved for this definition. Is using sum types the preferred approach, even in the more general situation where you might have many match branches, possibly introducing new variables? For example, suppose I didn't want baz n to equal bar n when foo n = cons m ls, but instead to equal m + bar n. I could make do with more sum and product types:
Definition is_cons : forall ls : list nat, {x | ls = cons (fst x) (snd x)} + { ls = nil }.
Proof. destruct ls eqn:K. now right. now left; exists (n,l). Qed.
Definition baz (n : nat) : nat.
refine (if is_cons (foo n) then _ else 42). destruct s as [(m,ls) H].
refine (m + bar n _); congruence. Defined.
and work from there, although even this gets a bit inelegant.
Karl Palmskog (Mar 22 2024 at 07:48):standard advice: use Equations to write any pattern matching definitions, then you for example get equational theorems with info from (implicit) matches for free
Pierre Courtieu (Mar 22 2024 at 07:53):Or if you allow yourself to use destruct, you can use `destruct H eqn:heqˋ
Justin Kelm (Mar 22 2024 at 08:16):Pierre Courtieu said:
Or if you allow yourself to use destruct, you can use `destruct H eqn:heqˋ
That appears to amount to the same thing behind the scenes as my first definition of baz, with the same problems about unfolding and destructing it later.
Johannes Hostert (Mar 22 2024 at 09:01):Sometimes it's possible to generalize the definition (so that it no longer mentions eq_refl). In your case it is:
Definition baz' (n : nat) (p : list nat) (Hp : foo n = p) : nat.
refine (match p as x return foo n = x -> nat with
| nil => fun _ => 42
| _ => _ end Hp).
intro; apply (bar n). rewrite H. apply cons_nil_ne. Defined.
Lemma eqeq n : baz n = baz' n (foo n) eq_refl.
Proof. reflexivity. Qed.
Theorem baz'_fact : forall n p Hp, baz' n p Hp <> 0.
Proof. intros; unfold baz'. destruct p; try congruence. apply bar_fact. Qed.
Now baz_fact follows from baz'_fact and eqeq.
Li-yao (Mar 22 2024 at 10:24):This seems to be something of an unnatural solution to a problem that arises naturally among beginners.
That solution is not as unnatural as it may seem at a glance. In fact it's the same trick (return foo n = x -> _, aka. the convoy pattern, or "abstract over an equality proof before destructing"), replicated at the proof level, modulo a small generalization that the return clause may also mention the proof of equality (return forall e : foo n = x -> _).
Last updated: Oct 13 2024 at 01:02 UTC