coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Accessibility for tuples of accessible values
- Date: Sun, 12 Apr 2020 22:17:46 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
- Ironport-phdr: 9a23:tjGVQRN4v6la9jUbLUcl6mtUPXoX/o7sNwtQ0KIMzox0K/r8rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6msZHQy6Pg5oLMz0HJTThoK5zbOc4ZrWNipBBya0Z4RdLRG8oB/N/p0ZiIZ+I6B3xRrNqHZSZ8xNxnJzJlOWmhvmoMG94MgwoGxrp/s9+psYAu3BdKMiQOkAVWl0AyUO/MTu8CL7Y06P638bCDlEiBdMChmctFf/V5b19CTzsOZ8ni+XIZ+uFOxmaXGZ965uDSTQpmIfLTdgrjPMid1rj6NepR+74Rpy39yMOdDHBL9FZqrYOOgiay9EV8dVWTZGB9riPZAMHvECPONdopO7oVYS/0Kz
That's not something you can prove. For instance if both RA and RB are < on nat, you have a loop
(0,1) < (1,0) (by left)
(1,0) < (0,1) (by right)
You need to use a lexicographic order instead.
Gaëtan Gilbert
On 12/04/2020 22:11, Carl Patenaude-Poulin wrote:
Hi coq-club! I'm a Coq hobbyist looking for technical guidance. I hope this is
a good place for this, if not I would appreciate being pointed in the right
direction!
Today, I am working on showing that a function recursing structurally on
either of two inductive parameters will always terminate. Here is my
development:
```
Section disjunct_relation.
Context {A B: Type}.
Context {RA: relation A}.
Context {RB: relation B}.
Definition disjunct_relation :=
fun x y => RA (fst x) (fst y) \/ RB (snd x) (snd y).
Theorem disjunct_relation_acc {a b}:
Acc RA a -> Acc RB b -> Acc disjunct_relation (a, b).
Admitted.
End disjunct_relation.
```
I'm struggling to put together a proof of `disjunct_relation_acc`. Do you have
suggestions for learning material that could help me sharpen my intuition on
how to approach proofs that involve non-trivial induction? I've already worked
through the first volume of Software Foundations, and also both of Adam
Chlipala's books.
I'd also like to hear about how people here approach thornier proofs. Do you
hash them out with pen and paper first? What intermediate steps can help you
understand the problem better before attempting an implementation?
Thank you in advance for your patient attention -
Carl Patenaude-Poulin
- [Coq-Club] Accessibility for tuples of accessible values, Carl Patenaude-Poulin, 04/12/2020
- Re: [Coq-Club] Accessibility for tuples of accessible values, Gaëtan Gilbert, 04/12/2020
Archive powered by MHonArc 2.6.18.