I need to prove some proposition for a small range a<=z<b of Z and the only way to prove this is by proving it separately for all values of Z in the range (which is then automated). Does someone have an elegant way to to destruct the goal into the b-a separate cases, say a specialized induction scheme? I guess one can do it reasonably elegant with mathcomp big-Op notations for and, but I would prefer to stay without mathcomp for my current project.

Currently I convert z-a to a nat n and destruct n until n+a>=b, but it is a bit messy.

spontaneously, it sounds like something you could/should program in MetaCoq (generation of the custom principle), since one wouldn't want a specific induction principle like that in a library. Either that or a regular plugin?

Either that or a regular plugin?

Hmm, I think this is more complicated than necessary. I was more thinking about a gallina function which evaluates to something like `P 0 /\ P 1 /\ P 2 ... /\ P n -> (forall z, 0<=z<=n -> P z)`

and then simply apply this and do a `repeat split`

.

The Gallina approach indeed seems to work. The proof of `range_split`

shouldn't be too hard.

```
From Coq Require Import ZArith.
Local Open Scope Z_scope.
Section range_split.
Context (a b : Z) (P : Z -> Prop).
(* Want to prove forall z, a <= z < b -> P z. *)
Fixpoint Hyps (n : nat) : Prop := match n with
| O => True
| S n => Hyps n /\ P (a + Z.of_nat n) (* will be left-nested conjunctions *)
end.
Theorem range_split : Hyps (Z.to_nat (b - a)) -> forall z, a <= z < b -> P z.
Admitted.
End range_split.
Lemma test (P : Z -> Prop) (H3 : P 3) (H4 : P 4) : forall z, 3 <= z < 5 -> P z.
apply (range_split 3 5 P); repeat split; assumption.
Qed.
```

The first part of the statement seems " foldr True and (map P (seq 0 n))"?

(or such)

@Jasper Hugunin : indeed this is easy to prove and it is much smoother to use than I thought. I didn't expect that the idea would work that directly. Please note that you can say `apply (range_split 3 5)`

without giving P explicitly - Coq apply is usually able to figure this out even in complicated cases. In your example case this is not a big thing, but in real applications where the goal could be huge it is. I will give it a test in complicated cases.

What I am wondering is if `induction`

is generally more powerful in figuring out the proposition or if it is more or less the same as `apply`

. In the latter case your solution is just fine. In the first case one should probably bring it into a form which can be used with `induction ... using ...`

.

Here is the proof (without @Paolo Giarrusso´s suggestion to make it more functional - one would need an additional lambda to add `a`

and then it is not much shorter / more readable than the fixpoint any more - at least to my physicists eyes)

```
From Coq Require Import ZArith.
Local Open Scope Z_scope.
Require Import Lia.
Section range_enumerate_cases.
Context (a b : Z) (P : Z -> Prop).
(* Want to prove forall z, a <= z < b -> P z. *)
Fixpoint Hyps (n : nat) : Prop := match n with
| O => True
| S n => Hyps n /\ P (a + Z.of_nat n) (* will be left-nested conjunctions *)
end.
Theorem range_enumerate_cases : Hyps (Z.to_nat (b - a)) -> forall z, a <= z < b -> P z.
Proof.
(* Eliminate the case a>=b *)
destruct (Z.lt_decidable a b) as [Hdec|Hdec].
2: (* range invalid *) lia.
(* replace b with n for easier induction *)
remember (Z.to_nat (b - a)) as n.
assert (b=a+Z.of_nat n) as Hbofn by lia. rewrite Hbofn.
clear Hbofn Heqn Hdec b.
induction n.
- (* a <= z < a *) lia.
- intros Hhyps z Hrange.
cbn in Hhyps. destruct Hhyps as [HhypsL HhypsR].
(* split the z range between HhypsL and HhypsR *)
destruct (Z.lt_decidable z (a + Z.of_nat n)) as [Hdec|Hdec].
+ specialize (IHn HhypsL). apply IHn. lia.
+ assert (z=a + Z.of_nat n) by lia; subst.
exact HhypsR.
Qed.
End range_enumerate_cases.
Lemma test (P : Z -> Prop) (H3 : P 3) (H4 : P 4) : forall z, 3 <= z < 5 -> P z.
Proof.
apply (range_enumerate_cases 3 5). cbv. repeat split; assumption.
Qed.
```

I gave it a few test runs. In complicated situations apply is not smart enough to figure out P and even with eapply it does not really work. If I give P explicitly - unfortunately a huge term - it does work, though.

Another issue is with repeat split: when I have a goal which is a conjunction, it also splits up that one.

I need to think about how to make this an induction scheme which can be used with `induction ... using ...`

. From a gut feeling I would say that induction would be smart enough to figure out P. Or maybe a better unification algorithm from UniCoq would help - not sure how I would use this without Mtac2.

Do apply: or refine do any better? They use evarconv instead of tactic unification

@Michael Soegtrop can't you use `match goal`

to extract the predicate?

If you rename `range_enumerate_cases`

to `range_enumerate_cases_uncurried`

, the below code performs the currying so that when used with `apply`

, you don't have to use `split`

afterwards.

```
Fixpoint curried_Hyps (n : nat) (Q : Prop) : Prop := match n with
| O => Q
| S n => curried_Hyps n (P (a + Z.of_nat n) -> Q)
end.
Lemma to_curried (n : nat) : forall (Q : Prop), (Hyps n -> Q) -> curried_Hyps n Q.
Proof.
induction n.
- intros Q f. exact (f I).
- intros Q f. apply IHn. intros; apply f. split; assumption.
Qed.
Theorem range_enumerate_cases : curried_Hyps (Z.to_nat (b - a)) (forall z, a <= z < b -> P z).
Proof.
apply to_curried.
apply range_enumerate_cases_uncurried.
Qed.
```

I also played around with `induction`

a little bit, but it doesn't seemed designed to work with a side condition like `a <= z < b`

. Induction schemes like `Zlt_0_rec`

seem to have the same problem, unless I'm misunderstanding how to use them.

I generally wonder: (1) how does induction infer P when apply can't? I know higher-order unification is hard, but that's not a full answer. Does induction simply abstract over the argument? (2) many induction principles aren't applicable with induction (see: Combined Scheme for mutual induction), but can one reuse induction's inference logic here? The workarounds are somewhat annoying.

Pierre-Marie Pédrot said:

Michael Soegtrop can't you use

`match goal`

to extract the predicate?

Possibly, but the higher order matching of Ltac1 is not that powerful either. I don't have a lot of experience with Ltac2 and Mtac2 in this respect as yet.

On the other hand the manual tactics to replace z with n and destruct n also work. I guess one could use a similar approach to create `P z`

with a tactic.

Would... pattern be useful? I've never found a real usecase in the wild, but it does seem relevant

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.pattern

For "induction n", starting with pattern n finds all the occurrences of n in the goal.

If you want occurrences in the context as well (and... I guess you do?), generalize dependent n might also be useful.

In both cases, the result seems regular enough for Ltac1 to match on.

Paolo Giarrusso said:

Would... pattern be useful? I've never found a real usecase in the wild, but it does seem relevant

Indeed the `pattern`

tactic might be very useful to construct `P z`

from the current goal in a reliable way. Possibly induction does something like this. I will do some experiments - also around @Jasper Hugunin ´s neat suggestion around Currying the hypothesis.

The `pattern`

tactic works well to prepare the goal and the Curried variant indeed helps to get exactly the goals I want. All very nice :-)

The only remaining problem I have is that usually (not always) I have the range condition `a <= z < b`

as hypothesis and it would be most convenient to have a tactic which simply gets such a hypothesis as argument in such cases. So instead of having the `forall z, a <= z < b`

in the end I would prefer to have `z`

and `a <= z < b`

as argument of the `range_enumerate_cases`

lemma before the Hyps. I can du this easily for the uncurried case but I fail to see how I would formulate / prove the `to_curried`

lemma in this case.

It is not a hard change to move the `forall z, a <= z < b ->`

quantifiers in front for `range_enumerate_cases`

. It just becomes

```
Theorem range_enumerate_cases : forall z, a <= z < b -> curried_Hyps (Z.to_nat (b - a)) (P z).
Proof.
intros z H.
apply to_curried; intros hyps.
exact (range_enumerate_cases_uncurried hyps z H).
Qed.
```

My whole file now looks like

```
From Coq Require Import ZArith.
Local Open Scope Z_scope.
Require Import Lia.
Section range_enumerate_cases.
Context (a b : Z) (P : Z -> Prop).
(* Want to prove forall z, a <= z < b -> P z. *)
Fixpoint Hyps (n : nat) : Prop := match n with
| O => True
| S n => Hyps n /\ P (a + Z.of_nat n) (* will be left-nested conjunctions *)
end.
Theorem range_enumerate_cases_uncurried : Hyps (Z.to_nat (b - a)) -> forall z, a <= z < b -> P z.
Proof.
(* Eliminate the case a>=b *)
destruct (Z.lt_decidable a b) as [Hdec|Hdec].
2: (* range invalid *) lia.
(* replace b with n for easier induction *)
remember (Z.to_nat (b - a)) as n.
assert (b=a+Z.of_nat n) as Hbofn by lia. rewrite Hbofn.
clear Hbofn Heqn Hdec b.
induction n.
- (* a <= z < a *) lia.
- intros Hhyps z Hrange.
cbn in Hhyps. destruct Hhyps as [HhypsL HhypsR].
(* split the z range between HhypsL and HhypsR *)
destruct (Z.lt_decidable z (a + Z.of_nat n)) as [Hdec|Hdec].
+ specialize (IHn HhypsL). apply IHn. lia.
+ assert (z=a + Z.of_nat n) by lia; subst.
exact HhypsR.
Qed.
Fixpoint curried_Hyps (n : nat) (Q : Prop) : Prop := match n with
| O => Q
| S n => curried_Hyps n (P (a + Z.of_nat n) -> Q)
end.
Lemma to_curried (n : nat) : forall (Q : Prop), (Hyps n -> Q) -> curried_Hyps n Q.
Proof.
induction n as [|n IHn].
- intros Q f. exact (f I).
- intros Q f. apply IHn.
intros; apply f. split; assumption.
Qed.
Theorem range_enumerate_cases : forall z, a <= z < b -> curried_Hyps (Z.to_nat (b - a)) (P z).
Proof.
intros z H.
apply to_curried; intros hyps.
exact (range_enumerate_cases_uncurried hyps z H).
Qed.
End range_enumerate_cases.
Lemma test (P : Z -> Prop) (H3 : P 3) (H4 : P 4) : forall z, 3 <= z < 5 -> P z.
Proof.
intros z H.
apply (range_enumerate_cases 3 5 _ z H). all: assumption.
Qed.
```

@Jasper Hugunin : thanks! Looking at your solution I now don't see how I could have messed it up. I guess I did too much C programming in my career and still don't have the true functional programmer mindset. I am working on it ...

I need to prove some proposition for a small range a<=z<b of Z

Suppose now that the range is not small. Generating a large number of subgoals doesn't sound very smart (and indeed I tried it and it wasn't successful). Is there a smarter way of proving such a statement by computation?

If your subgoals are decidable, you could write a decision procedure, and then run it with vm_compute or such. That would be a function `check : Z -> bool`

such that `check z = true -> P z`

, and then you chain that together to get a function `check_range : forall (a b : Z), bool`

such that `check_range a b = true -> forall z, a <= z < b -> P z`

, where check_range works by iterating through all the possibilities.

I'm sorry, but I don't think I understand what "iterating through all the possibilities" means here in practice. Wouldn't that also generate a large number of subgoals?

Not exactly. The idea goes something like: you have a function `range : Z -> Z -> list Z`

such that `range a b`

returns `[a; a+1; a+2; ...; b - 2; b-1]`

, and then `Definition check_range a b := forallb check (range a b)`

. Assuming you then prove `check_range_sound : check_range a b = true -> forall z, a <= z < b -> P z`

, you can use this simply by `apply (check_range_sound a b eq_refl)`

. No subgoals, just computation. (And you might be able to speed up the computation by using vm_compute in there somewhere).

If instead you have so many cases that computing all of them separately is prohibitive, you will need an entirely different strategy. Then I would ask: why do you believe this (that `a <= z < b -> P z`

) to be true? It can't be because you checked every case, there are too many of them. So you have to identify what other reason you have for believing this, and structure your proof that way.

Actually, if you are able to write a function `range : Z -> Z -> list Z`

(and prove it correct), then you are also able to directly write the function `check_range`

, without creating the whole list, which might be long. Here is a concrete example, where we enumerate 125 floating-point numbers (the code is a bit old and ugly, sorry): https://gitlab.inria.fr/flocq/flocq/-/blob/master/examples/Sqrt_sqr.v#L1660

why do you believe this (that a <= z < b -> P z) to be true?

Because I have a Coq proof of it, but it's more than 200 lines of code and takes about 5 minutes to compile. It was a very hard proof to come up in the first place because there is little structure to the theorem, or rather, the reason the theorem holds changes in hard-to-predict ways depending on the sub-range in question. I don't *need* to come up with a computation proof (and it's looking like any such proof would take significantly longer than 5 minutes to compile anyway), but I will have other similar results to prove and it would be nice to know how to do it, if it's possible at all.

(You may ask: how did you even come up with a theorem statement for something so weird? And the answer is that I didn't; I'm formalizing someone else's work, and since they were not restricted to Coq, they "proved" it by checking all the cases in some fast programming language)

Actually, if you are able to write a function range : Z -> Z -> list Z (and prove it correct), then you are also able to directly write the function check_range, without creating the whole list, which might be long.

In this case it would definitely be long, yes! Thank you very much, I will take a look

Note that creating the list is long, but it is still only a fraction of the overall computation, since the computation has to create all the integer values anyway. The issue is more that all these values hog memory. For example, it takes less than one second to create a list containing 1 million integers:

```
Time Eval vm_compute in
let '(l,i) :=
Pos.iter (fun '(l,i) => (cons i l, Z.succ i)) (nil,0%Z) 1000000%positive in
Z.of_nat (length l).
```

@Ana de Almeida Borges if vm_compute is too slow, you could also use native_compute.

Or you could write the checker in Coq, prove it correct, and extract it to OCaml.

@Jasper Hugunin we ended up implementing your suggestions and the resulting tactics were extremely helpful (and very fast)! We made the tactics available as an opam package called `coq-formalv-check_range`

, see also the source code.

Last updated: May 24 2024 at 22:02 UTC