Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Accessibility for tuples of accessible values

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Accessibility for tuples of accessible values


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page