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.

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

Note that mutual recursion can be eliminated through indices.

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

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.

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:

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

@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 ...

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:

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/).

Getting coq*IDE* might add complications?

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

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.

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

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

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

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

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

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

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).

Fixed the load-path problem. Going for the `Scheme`

s.

@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

See Lemma form_prog_dec :

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

and you phrase that as one lemma

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

(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 )

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

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`

(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)

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:

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.

Replacing `*`

with `/\`

and then just applying the induction rule resulting from the combined scheme solved it. Thanks a ton, guys.

Last updated: Oct 13 2024 at 01:02 UTC