Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dependent types

view this post on Zulip Email Gateway (Aug 18 2022 at 15:00):

From: Lawrence Paulson <lp15@cam.ac.uk>
I think that this particular definition means nothing more than the following:

inductive
mkMyNum :: "[nat list, nat list] => bool"
where
M: "mkMyNum xs (n#xs)"

Larry Paulson

view this post on Zulip Email Gateway (Aug 18 2022 at 15:09):

From: Ian Lynagh <igloo@earth.li>
Hi all,

I have some coq proofs that I am considering converting to Isabelle.
However, the coq proofs use dependent types, similar to this:

Inductive MyNum (from : list nat) (to : list nat) : Type
:= mkMyNum : forall (myNum : nat)
(valid : to = cons myNum from),
MyNum from to.

Can anyone tell me what the best way to handle this in Isabelle would be
please?

Thanks
Ian

view this post on Zulip Email Gateway (Aug 18 2022 at 15:11):

From: Tobias Nipkow <nipkow@in.tum.de>
I don't speak Coq very well, but if this defines some subset of nat
lists, the conversion may work according to the following general
schema: replace the dependent type by some unconstrained type (eg nat
list), introduce predicates that check that some nat list satisfies the
constraints in the dependent type, and make those predicates
preconditions in your theorems whenever needed. You recast the type
constraints as explicit formulas.

Tobias

Ian Lynagh wrote:

Last updated: Apr 25 2024 at 20:15 UTC