Michael Soegtrop (Nov 02 2020 at 14:53): Michael Soegtrop (Nov 02 2020 at 14:53):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.
Karl Palmskog (Nov 02 2020 at 15:36):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?
Michael Soegtrop (Nov 02 2020 at 18:39):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.
Jasper Hugunin (Nov 02 2020 at 19:06):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))"?
Paolo Giarrusso (Nov 02 2020 at 19:08):(or such)
Michael Soegtrop (Nov 03 2020 at 08:58):@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.
Paolo Giarrusso (Nov 03 2020 at 10:54):Do apply: or refine do any better? They use evarconv instead of tactic unification
Pierre-Marie Pédrot (Nov 03 2020 at 12:22):@Michael Soegtrop can't you use match goal to extract the predicate?
Jasper Hugunin (Nov 03 2020 at 16:51):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.
Paolo Giarrusso (Nov 03 2020 at 18:39):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.
Michael Soegtrop (Nov 03 2020 at 20:55):Pierre-Marie Pédrot said:
Michael Soegtrop can't you use
match goalto 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.
Paolo Giarrusso (Nov 03 2020 at 21:02):Would... pattern be useful? I've never found a real usecase in the wild, but it does seem relevant
Paolo Giarrusso (Nov 03 2020 at 21:02):https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.pattern
Paolo Giarrusso (Nov 03 2020 at 21:02):For "induction n", starting with pattern n finds all the occurrences of n in the goal.
Paolo Giarrusso (Nov 03 2020 at 21:03):If you want occurrences in the context as well (and... I guess you do?), generalize dependent n might also be useful.
Paolo Giarrusso (Nov 03 2020 at 21:04):In both cases, the result seems regular enough for Ltac1 to match on.
Michael Soegtrop (Nov 04 2020 at 08:25):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.
Michael Soegtrop (Nov 04 2020 at 11:37):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.
Jasper Hugunin (Nov 04 2020 at 18:04):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 ...
Ana de Almeida Borges (Jan 21 2021 at 17:46):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?
Jasper Hugunin (Jan 21 2021 at 18:02):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.
Ana de Almeida Borges (Jan 21 2021 at 18:22):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?
Jasper Hugunin (Jan 21 2021 at 18:29):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).
Jasper Hugunin (Jan 21 2021 at 18:32):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.
Guillaume Melquiond (Jan 21 2021 at 18:43):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
Ana de Almeida Borges (Jan 21 2021 at 18:48):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)
Ana de Almeida Borges (Jan 21 2021 at 18:53):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
Guillaume Melquiond (Jan 21 2021 at 20:00):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.
Paolo Giarrusso (Jan 22 2021 at 00:09):Or you could write the checker in Coq, prove it correct, and extract it to OCaml.
Ana de Almeida Borges (Jul 26 2022 at 09:17):@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: Sep 23 2023 at 07:01 UTC