during a discussion meandering a bot off topic at Adding more trigonometry in Reals I found that one is forced to supply patterns to a match which don’t type check. A piece from the linked discussion demonstrating this is:
Require Import Vector.
Import VectorNotations.
Import Fin.
Inductive sumn (n : nat) (P : Vector.t Prop n) : Set :=
sumi (i : Fin.t n) (p : Vector.nth P i) : sumn n P.
Lemma lt_eq_lt_dec_1: forall n m : nat, sumn 3 [ n < m; n = m; m < n ].
Proof.
intros n m.
pose proof Compare_dec.lt_eq_lt_dec n m as H.
destruct H as [[H|H]|H].
apply (sumi _ _ F1); assumption.
apply (sumi _ _ (FS F1)); assumption.
apply (sumi _ _ (FS (FS F1))); assumption.
Qed.
Definition match_typechecktest (n m : nat) : nat :=
match lt_eq_lt_dec_1 n m with
| sumi _ _ (FS (FS (FS F1))) _ => 1
| sumi _ _ _ _ => 0
end.
Obviously the type of lt_eq_lt_dec_1 n m is sumn 3 ... while the first pattern would only typecheck against a sumn n ... for n>=4.
Looking at the typing rule for match at The match … with … end construction I must admit I didn’t see where the type of the constructor arguments is defined - as physicist I find this still a bit hard to read. But I guess for correctness it is not required that the match pattern arguments have the correct type - the match patterns just need to be structurally complete.
But I wonder if there is a dependent match which would allow to discard all patterns which don’t type check and if this doesn’t exist, what it would take to implement it. I could imagine that there are no other places in the kernel where the type checking of a term depends on that a certain term does not type check. On the other hand the dependent destruction tactic gets this right and ends up (applied repeatedly) with the 3 possibilities one would expect for a sumn 3 (see the first link for an example).
But I wonder if there is a dependent match which would allow to discard all patterns which don’t type check and if this doesn’t exist, what it would take to implement it.
I believe this is one the purposes of the Program and Equations plugins.
My understanding of match is that it is meant to be as simple as possible for the purpose of keeping the kernel small and trustworthy, which does not necessarily make it easy to use.
It is hard to decide in general whether a pattern “type checks”, because it can have arbitrary terms as indices. Instead of putting arbitrary incomplete heuristics in the kernel, they can live in a desugaring/elaboration phase between the surface syntax programmers write, and the core language the kernel interprets.
Thus match is really a low-level construct, and more ergonomic variants are meant to be defined on top of that, such as what can be found in the Program and Equations plugins. Even the match ... with we usually write must be elaborated into the actual match ... in ... return ... with in the core language.
If you don’t write dependently-typed functions, you won’t ever notice the issue. Sometimes I wonder whether that’s a compelling enough reason to discourage writing programs with dependent types in Coq, and only use dependent types as propositions without mentioning that’s what they are.
It is not rare to hear “yes, Coq is dependently typed, but don’t use it!”. I discussed this with some of the experts at INRIA and the answer I mostly get is that it can be definitely improved, but no one can say how usable it would be then without doing so. I guess it is a hen and egg problem: people find dependent types awkward to use, so this is not used much and as a result there are not that many requests to improve this. Maybe this changes with Equations. Making working with dependent types easier likely improves requests for doing so employing different styles.
Indeed I meant a separate dependent match construct which would relate to match as dependent destruction relates to destruct. But I guess this would require an axiom since the dependent destruction tactic requires the John Major equality axiom and afaik the Equations plugin uses Axiom K. An interesting question to me is if this would be implemented in the kernel match if this would be weaker than JMeq_eq or axiom K. I hope this makes sense - I am physicist and not a logician.
I can imagine how this function written using the Equations plugin would look like, but I am not sure how Program could help here. Are you aware of any construct which gets syntactically close to a match statement?
I can imagine how this function written using the Equations plugin would look like, but I am not sure how Program could help here. Are you aware of any construct which gets syntactically close to a match statement?
Program can automatically discharge absurd obligations. In the following example, you only need to define the cases that matter (where i : Fin.t 3). You still have to put an underscore for the other absurd cases, but it gets filled out automatically by Program.
Require Import Program.
Program Definition match_typechecktest (n m : nat) : nat :=
match lt_eq_lt_dec_1 n m with
| sumi _ _ i _ =>
match i return nat with
| F1 | FS F1 | FS (FS F1) => 0
| _ => _
end
end.
the Equations plugin uses Axiom K
I think the issue of axioms is a red herring. It raises some theoretical questions, but practically, fixing these systems to not use those axioms, at an insignificant cost in applicability, seems:
not hard conceptually
but it will take some engineering effort
and the reward is meager (it’s merely an implementation detail, most users can just pretend that axiom is not there)
Neat! A very nice example of using Program. And it does not use axioms (I checked with Print Assumptions on your definition).Thanks for pointing this out - I would say this is good enough.
well there is the issue that e.g. axiom K is incompatible with univalence. See the post by @Zimmi48: