Email Gateway (Aug 19 2022 at 17:32): Email Gateway (Aug 19 2022 at 17:32):From: Andrew Gacek <andrew.gacek@gmail.com>
I'm playing around with quotients in Isabelle/HOL, but I'm having a
hard time getting the 'descending' tactic to work. I've tried
following the examples in the distribution, but perhaps I missed a key
step. Here's my simple example:
theory Scratch
imports Main
begin
definition z3_rel :: "int ⇒ int ⇒ bool" (infix "\<approx>" 50) where
[simp]: "z3_rel x y = (3 dvd (x - y))"
quotient_type z3 = int / z3_rel
apply (rule equivpI)
apply (rule reflpI, simp)
apply (rule sympI, simp, presburger)
apply (rule transpI, simp, presburger)
done
quotient_definition sum where "sum :: z3 ⇒ z3 ⇒ z3" is "plus :: int ⇒ int ⇒ int"
by (simp, presburger)
lemma sum_assoc:
"sum (sum a b) c = sum a (sum b c)"
apply descending
(* exception UnequalLengths raised (line 569 of "library.ML") *)
Thanks,
Andrew
Email Gateway (Aug 22 2022 at 08:59):From: Andrew Gacek <andrew.gacek@gmail.com>
I never found a solution to this, but I did find two workarounds.
Manually state the descended lemmas and then use the lifting tactic
to prove the desired lemmas. This gets tedious.
Use nat instead of int. I don't know why this works, but descending
just seems to work better with nat instead of int. The downside is
that some definitions are more complicated since subtraction on
naturals does not have as many nice algebraic properties as
subtraction on integers.
-Andrew
Email Gateway (Aug 22 2022 at 08:59):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Andrew,
The quotient package with the quotient_definition command is in large parts superseeded by
the lifting and transfer packages, as said in the isar-ref manual (section 11.7). If your
application does not fall into the rare cases where the quotient package is needed, I
recommend that you do your constant definitions with lift_definition rather than quotient
definition. Then, you can use the proof method transfer instead of descending. In your
example. lift_definition+transfer works fine.
The problem with int is that the int type itself is defined as a quotient over nat * nat,
as can be seen from the diagnostic command print_quotientsQ3. Thus, the descending method
gets confused about how far it should descend. This is probably also the reason for the
exception.
Best,
Andreas
Last updated: Apr 19 2024 at 08:19 UTC