Stream: Coq users

Topic: Circular recursive definition

Mohammad-Ali A'RÂBI (Sep 24 2020 at 16:43):

Hello people. I have two terms, namely 𝔗 and 𝔄, that are recursively defined, but then in their definition, each one depends on the other:
Definitions-of-A-and-T.png

Now, when I do induction on 𝔗, I have to deal with 𝔄 at the end, and vice versa. Any ideas on how can I do inductions?
For reference, please take a look at this branch of my repo.

Li-yao (Sep 24 2020 at 16:58):

You can do mutually recursive definitions (though it's far from easy to make it work), here's an example: https://coq.inria.fr/distrib/current/refman/language/core/inductive.html#example-mutual-fixpoints

Pierre-Marie Pédrot (Sep 24 2020 at 17:11):

Note that mutual recursion can be eliminated through indices.

Pierre-Marie Pédrot (Sep 24 2020 at 17:12):

You can typically write a type Inductive I (_ : bool) := ... where the index set to true encodes for T types and set to false for A types

Christian Doczkal (Sep 25 2020 at 13:12):

Here is another example that is maybe closer to your use-case, namely the formulas and programs of propositional dynamic logic (PDL): https://github.com/coq-community/comp-dec-modal/blob/master/PDL/PDL_def.v

If your syntax is mutually recursive, you will likely anyways want to simultaneously prove two statements, one for each of the two types. In the case where all you need are propositions, then Combined Scheme should do the trick. If some of your "statements" actually have sort "Type" you may have to create the combined scheme manually as I did here.

I suppose that using the indexed approach, you will have theorem statements involving if/match clauses to separate the two types. This may or may not be what you want. In the end, it's probably a matter of taste.

Christian Doczkal (Sep 25 2020 at 13:18):

Mohammad-Ali A'RÂBI said:

For reference, please take a look at this branch of my repo.

I suggest using a more modern version of Coq than 8.4pl3. The difference between 8.4 and the current 8.12 release is quite significant. :fear:

Pierre-Marie Pédrot (Sep 25 2020 at 13:19):

The difference between 8.4 and 8.5 alone is already very significant.

Christian Doczkal (Sep 25 2020 at 13:30):

@Pierre-Marie Pédrot I think the first version of Coq I used was 8.3, and I don't recall the major change from 8.4 to 8.5. Long time ago ...

Mohammad-Ali A'RÂBI (Sep 26 2020 at 23:00):

Thanks a lot, people. I'm unable to install the latest CoqIDE on my Ubuntu 14.04, but I'll have to upgrade my OS eventually. :grinning_face_with_smiling_eyes:

The Scheme should do the trick, but I have to study it deeper. Still don't know how does it work. :thinking:

Théo Zimmermann (Sep 27 2020 at 09:23):

There are many alternatives to your system package manager to get a more recent version of Coq. The most common one is using opam: see https://coq.inria.fr/opam-using.html. But be aware that you would need opam 2 which is not the version you can get through your package manager on an old Ubuntu. You can also get the latest version of Coq through Conda (https://conda-forge.org/) or Nix (https://nixos.org/).

Paolo Giarrusso (Sep 27 2020 at 09:54):

Getting coqIDE might add complications?

Paolo Giarrusso (Sep 27 2020 at 09:55):

@Christian Doczkal IIRC Combined Scheme now works on Type as well, but surely not in 8.4

Mohammad-Ali A'RÂBI (Sep 27 2020 at 10:56):

I managed to install opam 2.0.4 on my system, but CoqIDE 8.12.0 requires conf-gtk3 18, which also, in turn, requires gtk+-3.0 to be install, and as it seems, the latest one compatible to Ubuntu 14.04 is not sufficient.

Coq 8.12.0 itself is installed with no problem.

Paolo Giarrusso (Sep 27 2020 at 12:29):

There are plugins to use Coq from Emacs, Vi, and vscode. The Emacs one is the most commonly used.

Paolo Giarrusso (Sep 27 2020 at 12:30):

Another way is that CoqIDE is relatively independent of the actual Coq version

Paolo Giarrusso (Sep 27 2020 at 12:31):

Finally, the latest coqide using gtk2 is much more recent than 8.4

Paolo Giarrusso (Sep 27 2020 at 12:33):

(The “coqide is independent” part might be trickier to exploit, I’ve only read it on github)

Paolo Giarrusso (Sep 27 2020 at 12:34):

Coq 8.10 was the first version using gtk3, according to the manual: https://coq.inria.fr/distrib/current/refman/changes.html#version-8-10

Paolo Giarrusso (Sep 27 2020 at 12:36):

So 8.9 should be installable, and much closer to modern practice. (OTOH, 14.04 is probably outside its maintenance window)

Mohammad-Ali A'RÂBI (Sep 27 2020 at 22:22):

So, I installed Ubuntu 20.04 together with Coq and -IDE 8.12.0 (through opam). Made the makefile through CoqIDE, and it works fine, but the IDE itself cannot load the modules, saying it cannot find the .vos files (they are there, only empty).

Mohammad-Ali A'RÂBI (Sep 27 2020 at 22:35):

Fixed the load-path problem. Going for the Schemes.

Mohammad-Ali A'RÂBI (Oct 01 2020 at 22:44):

@Christian Doczkal I am still confused. I tried to imitate the combined schemes solution from here, but still don't know how to use them in the proof. The Coq's manual on schemes also has no examples of using them in the proofs.

If you can take a look at the current state of my progress, I would really appreciate it:
https://github.com/aerabi/lttt/blob/eea889489d4ea006158464c42c8948b27d07c641/BaseProofs.v#L73

Paolo Giarrusso (Oct 01 2020 at 23:51):

See Lemma form_prog_dec :

Paolo Giarrusso (Oct 01 2020 at 23:52):

Basically, what you can do is a simultaneous induction on your mutually inductive types T and U

Paolo Giarrusso (Oct 01 2020 at 23:54):

and you phrase that as one lemma

Paolo Giarrusso (Oct 01 2020 at 23:54):

you cannot use the induction tactic, but you can start by applying the combined induction scheme.

Paolo Giarrusso (Oct 01 2020 at 23:55):

(users of form_prog_ind might be a better example, like https://github.com/coq-community/comp-dec-modal/blob/master/PDL/PDL_def.v#L152 )

Paolo Giarrusso (Oct 01 2020 at 23:56):

to be able to apply the combined scheme, you should use About on it, identify its conclusion, and state the lemma so that it matches the conclusion

Paolo Giarrusso (Oct 01 2020 at 23:56):

in your case, the conclusion will probably have a form similar to (forall t: T, P1 t) /\ (forall u: U, P2 u) — and you need to pick the right P1 and P2

Paolo Giarrusso (Oct 01 2020 at 23:58):

(https://github.com/coq-community/comp-dec-modal/blob/master/PDL/PDL_def.v#L497 might be a slightly more typical example, tho I’m confused that it uses * and not /\, yet it uses the _ind principle)

Christian Doczkal (Oct 02 2020 at 07:25):

Paolo Giarrusso said:

(https://github.com/coq-community/comp-dec-modal/blob/master/PDL/PDL_def.v#L497 might be a slightly more typical example, tho I’m confused that it uses * and not /\, yet it uses the _ind principle)

Indeed, this is a bit obscure. The reason for phrasing the statement with a * is that this turns the statement into an ssreflect multirule for rewrite, even though this may not be used for this particular lemma. As for why this works, the apply: tactic actually, which is based on the same algorithm as refine, inserts a coercion from "A /\ B" to "A * B". This can be seen by running:

Goal forall A B : Prop, A /\ B -> A * B.
Unset Printing Notations.
intros A B AB. refine AB. Print Graph.
Show Proof.

which yields fun (A B : Prop) (AB : and A B) => pair_of_and AB. :shrug:

Christian Doczkal (Oct 02 2020 at 07:31):

Paolo Giarrusso said:

Christian Doczkal IIRC Combined Scheme now works on Type as well, but surely not in 8.4

I can confirm that Combined Scheme now works in Type at least in 8.12, let's see what CI says about older versions.

Mohammad-Ali A'RÂBI (Oct 05 2020 at 22:07):

Replacing * with /\ and then just applying the induction rule resulting from the combined scheme solved it. Thanks a ton, guys.

Last updated: Oct 03 2023 at 02:34 UTC