Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem copying logical relation from TAPL

Email Gateway (Aug 19 2022 at 16:39):

From: Clarissa Littler <clarissa.littler@gmail.com>
Hi,
So just as an exercise I was going to formalize ch 12 of Types and
Programming Languages and, well, I was defining the inductive relation for
reducibility candidates as

inductive R :: "lam ⇒ ty ⇒ bool" where
Ra : "⟦halts y; typing [] y A⟧ ⟹ R a A" |
RArr : "⟦halts l; (∀ y. R y ty1 ⟶ R (App l y) ty2); typing [] l (Arr ty1
ty2)⟧ ⟹ R l (Arr ty1 ty2)"

and I got the following error that I really don't know how to fix

Proof failed.

1. ⋀x y xa xb l ty1 ty2 ya.
   x (?x25 x y xa xb l ty1 ty2 ya) (?x26 x y xa xb l ty1 ty2 ya) ⟶
   y (?x25 x y xa xb l ty1 ty2 ya) (?x26 x y xa xb l ty1 ty2 ya) ⟹
   y ya ty1 ⟶ x ya ty1

2. ⋀x y xa xb l ty1 ty2 ya. x ≤ y ⟹ x (App l ya) ty2 ⟶ y (App l ya) ty2

3. ⋀x y xa xb l ty1 ty2. x ≤ y ⟹ typing [] l (Arr ty1 ty2) ⟶ typing [] l
   (Arr ty1 ty2)
   The error(s) above occurred for the goal statement⌂:
   mono (λp x1 x2.
   (∃y. x1 = a ∧ x2 = A ∧ halts y ∧ typing [] y A) ∨
   (∃l ty1 ty2.
   x1 = l ∧
   x2 = Arr ty1 ty2 ∧ halts l ∧ (∀y. p y ty1 ⟶ p (App l y) ty2) ∧
   typing [] l (Arr ty1 ty2)))

I'm guessing it's about negative recursion in the pre-condition of the RArr
rule, but that also seems to be exactly the definition that TAPL uses so
I'm not sure what's what.

Cheers,
Clarissa

Email Gateway (Aug 19 2022 at 16:40):

From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Clarissa,

Yes, indeed the negative occurrence is the stumbling block
for the inductive command. What you can do instead is define
the candidates by recursion over the type. Right now I am not
having TAPL available for the details, but I remember I followed
the strong normalisation proof in Girard's Proofs & Types book.
Maybe the file

isabelle/src/HOL/Nominal/Examples/SN.thy

where the candidates are defined around line 228 is of help to you.
You possibly need to ignore the nominal stuff there that is not really
important for the candidates definition. If I remember correctly
also somewhere in the sources or AFP is a similar proof by Stefan
Berghofer providing a definition for candidates.

Hope this helps,
Christian

Email Gateway (Aug 19 2022 at 16:40):

From: Clarissa Littler <clarissa.littler@gmail.com>
Ah, that makes perfect sense. The "negativeness" in the definition of
reducibility candidates just becomes recursive calls at a smaller type,
which primrec/fun will accept with no problem.

Thanks!

Last updated: Nov 21 2024 at 12:39 UTC