Karl Palmskog (Jul 09 2020 at 11:07): Karl Palmskog (Jul 09 2020 at 11:07):One limitation of cofix is that one can't use it to build anything other than coinductive types. So let's say I need to prove the existence of some term using cofix (i.e., I want to define a function whose result lives in Prop). Is the only option to define a coinductive predicate that mirrors ex, and has somebody done this before maybe?
Gaëtan Gilbert (Jul 09 2020 at 11:24):Can you give an example?
Karl Palmskog (Jul 09 2020 at 11:35):Suppose midpoint is a coinductive predicate.
Lemma ex_midpoint : forall (s1 s2: stmt) (st: state) (tr: trace)
(h: redm (Sseq s1 s2) st tr), exists tr, midpoint h tr.
Proof.
Fail cofix COINDHYP.
output:
The command has indeed failed with message:
All methods must construct elements in coinductive types.
do I need to define:
CoInductive exc (A:Type) (P:A -> Prop) : Prop :=
exc_intro : forall x:A, P x -> exc (A:=A) P.
or has somebody done this? What are the consequences?
Gaëtan Gilbert (Jul 09 2020 at 11:38):How would the recursive call be used? you can't project out of it during the cofixpoint.
Karl Palmskog (Jul 09 2020 at 11:39):there is a coinductive case in the midpoint predicate. I don't see how I can handle that case without coinduction, i.e., cofix.
Gaëtan Gilbert (Jul 09 2020 at 11:54):Try to write your proof with exc and see what happens
Paolo Giarrusso (Jul 09 2020 at 11:54):are traces finite or infinite? If it is infinite, can you actually provide it in one go?
Paolo Giarrusso (Jul 09 2020 at 11:55):I ask because, in general, the intuition I have from Agda codata is that coinduction creates infinite but productive computations, which can be run “step-wise”
Paolo Giarrusso (Jul 09 2020 at 11:56):so, make sure that your lemma can be proved that way.
Paolo Giarrusso (Jul 09 2020 at 11:57):For instance, if you were proving that finite reduction sequences can be extended into infinite ones (wild guess), that statement couldn’t do it I think, even with exc — you’d have to provide the trace steps one at a time
Karl Palmskog (Jul 09 2020 at 11:58):traces are possibly-infinite
Paolo Giarrusso (Jul 09 2020 at 11:59):_is_ the actual witness tr meant to be finite?
Karl Palmskog (Jul 09 2020 at 12:01):it could be infinite from my understanding, but doesn't have to be
Paolo Giarrusso (Jul 09 2020 at 12:02):I was wondering about the witness in the proof you have in mind, if you have one. If that’s, I’d maybe use an inductive version of midpoint, and try to prove that inductive midpoint implies the coinductive one (can you)? But I’m just brainstorming (per my usual), and lack experience with Coq coinduction
Simon Hudon (Jul 09 2020 at 12:40):I have struggled with the same thing. My best answer so far was to create a corecursive function that makes the witness, prove that it's a valid witness and then wrap the two in a single proof of the existential
Karl Palmskog (Jul 12 2020 at 11:22):I looked much deeper into this. The "create a corecursive witness function" approach works if your witness function doesn't much need to look at (do inversion on) stuff in Prop to do its job, i.e., it just builds something in Set with only plain destruct/match on things in Set.
However, the guardedness condition becomes a world of hurt when you need to do serious inversion on Props and thus return something like exists t : trace, P t, where P is a coinductive predicate on traces. Basically, to build the required trace coinductively, one usually:
t') to construct the required texists t, and then apply the coinductive predicate constructor to prove P t using the proof of P t' obtained before This is in the wrong order for the guardedness checker.
In contrast, if you just want return a plaintrace without exists, you can instead apply a coinductive constructor directly and then do the corecursive call, since you don't need further information (properties) on what the corecursive call returns at the "top level". This satisfies the guardedness condition.
In the end I resorted to constructive_indefinite_description to make my plain non-Prop witness function be able to do inversion on things in Prop and just return a plain trace. Before this, I also tried things like the recent coinduction plugin, but to no avail.
Here is the current sad state of non-constructiveness. Better ideas would be welcome.
Karl Palmskog (Aug 04 2020 at 12:22):I constructed a "minimal" example and wrote up the thing for the Disourse: https://coq.discourse.group/t/proving-existence-statements-about-coinductive-predicates-constructively/994
Simon Hudon (Aug 04 2020 at 15:01):What if you put ex_midpoint and follows in Set instead of Prop. Then exists tr, ... becomes { tr | ... } and you don't need to use choice on it anymore
Simon Hudon (Aug 04 2020 at 15:04):I feel like if you stay in Prop, whatever you construct could be used to prove skolemization on natural numbers
Karl Palmskog (Aug 04 2020 at 15:19):good observation, yes, everything works fine if you put follows in Set. But then you can't use impredicativity anymore, which seems like a bad tradeoff to me. Maybe some meta-theoretical argument like one on skolemization can indeed establish that impredicativity for these kinds of relations needs to be "bought" at the cost of constructive epsilon...
Karl Palmskog (Aug 04 2020 at 15:19):I should probably augment the Discourse post with that alternative though (even though I focus on Prop in the title).
Simon Hudon (Aug 04 2020 at 16:37):Where do you use impredicativity in your code?
Karl Palmskog (Aug 04 2020 at 16:51):it's used in the larger development at https://github.com/palmskog/coind-sem-while - see p. 14 footnote in https://arxiv.org/pdf/1412.6579.pdf
Karl Palmskog (Aug 04 2020 at 16:53):I don't have high stakes riding on this, but would be nice to say definitively if certain constructive Prop coinductive proofs can't be done, like we know "finite or infinite" can't be proven constructively (reduce to halting problem and so on).
Simon Hudon (Aug 04 2020 at 17:02):That's a really cool looking project! I'll have to look closer
Simon Hudon (Aug 04 2020 at 17:05):I was faced with a similar problem a while ago. I was proving the existence of refinement mapping in temporal logic. It boiled down, at every state of an infinite trace that there exists a suitable abstract state corresponding to the concrete state. That's where I concluded that there was no constructive solution to show that there exists a suitable abstract trace.
Simon Hudon (Aug 04 2020 at 17:05):With your case, I'm not sure if you need to show an infinite number of existentials for your traces or just one mid-point
Karl Palmskog (Aug 04 2020 at 17:14):sounds similar, but I'll have to think some more.
Karl Palmskog (Aug 04 2020 at 17:16):along the same lines as the repo I just mentioned, this is a library with more generic traces/properties I extracted out: https://github.com/palmskog/coind-traces
Last updated: Oct 13 2024 at 01:02 UTC