Stream: Beginner Questions

Topic: Can you convert from prop back to bool?


view this post on Zulip Isaac Oscar Gariano (Sep 30 2021 at 03:08):

I am curious, would something like this be admissiable in HOL:

axiomatization Proptrue :: ‹prop ⇒ bool›  where
  prop_iff_bool [simp]: ‹Trueprop (Proptrue P) ≡ P›

Then you can use meta-propositions in HOL ones, e.g:

lemma ‹Proptrue(P ⟹ Q) ⟶ (P ⟶  Q)› by(auto)

Sorry if this is a very dumb idea/question, I'm new to Isabelle!

view this post on Zulip Kevin Kappelmann (Sep 30 2021 at 10:52):

admissible is not the right word in this context since your axiomatisation adds theorems about a new constant that previously were not derivable (since the constant did not exist).

I suppose you are interested in whether this would introduce any inconsistencies. I think it would not but you better ask an expert on the mailing list if you want to be sure (or maybe @Simon Roßkopf knows a simple argument?)

In any case, it does not seem like a good idea to add such a constant. Reasoning in isar using meta level connectives is more convenient than using object level connectives.

view this post on Zulip Isaac Oscar Gariano (Sep 30 2021 at 21:36):

Yes your right, I did mean to say consistent, although now I wonder if this would be provable:

lemma LPropTrue:
  fixes p :: ‹prop›
  obtains b :: ‹bool› where ‹Trueprop b ≡ p›
sorry

I have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)

I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.

view this post on Zulip Isaac Oscar Gariano (Sep 30 2021 at 21:56):

Also, on a related note what got me thinking about Proptrue was me trying to make some syntax sugar, but it keeps wrapping things in Trueprop:

syntax "_foo" :: ‹prop ⇒ prop ⇒ prop'› (‹⫿_›)
parse_ast_translation ‹[("_foo", fn _ => fn [body] => body)]›

However prop ‹⫿P›, and even ‹(⫿(P :: prop)) :: prop› reports a type error

Operator:  Trueprop :: bool ⇒ prop
Operand:   P :: prop

Using declare [[syntax_ast_trace]] the AST is apparently:

 ("\<^const>HOL.Trueprop" ("_constrain" ("\<^const>HOL.Trueprop" ("_constrain" P <position>)) "\<^type>prop"))

Interstingly, if I don't use ML and instead do

translations "⫿P" ⇀ "P"

It works as expected, but that's not sufficient as I have more complicated desugarings I want to do.

view this post on Zulip Kevin Kappelmann (Sep 30 2021 at 23:02):

Isaac Oscar Gariano said:

Yes your right, I did mean to say consistent, although now I wonder if this would be provable:

lemma LPropTrue:
  fixes p :: ‹prop›
  obtains b :: ‹bool› where ‹Trueprop b ≡ p›
sorry

I have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)

I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.

That lemma is unprovable. The best you can do, given your axiomatisation for Proptrue, is this:

axiomatization Proptrue :: prop  bool  where
  prop_iff_bool [simp]: Trueprop (Proptrue (PROP P))  PROP P

lemma
  fixes p :: prop
  obtains Trueprop True  p | Trueprop False  p
proof -
  assume
    h1 : "Trueprop True ≡ p ⟹ thesis" and
    h2 : "Trueprop False ≡ p ⟹ thesis"
  have p_eq: "Trueprop (Proptrue p) ≡ p" by simp
  have
    h1' : "Trueprop True ≡ Trueprop (Proptrue p) ⟹ thesis" and
    h2' : "Trueprop False ≡ Trueprop (Proptrue p) ⟹ thesis" by
      (subst(asm) p_eq | fact h1 | fact h2)+
  show thesis
  proof (cases "Proptrue p")
    case True
    have "Trueprop True ≡ Trueprop (Proptrue p)" by (simp add: True)
    then show thesis by (rule h1')
  next
    case False
    hence "Trueprop False ≡ Trueprop (Proptrue p)" by simp
    then show thesis by (rule h2')
  qed
qed

view this post on Zulip Kevin Kappelmann (Sep 30 2021 at 23:04):

You can, in theory, axiomatise all HOL operators to live in prop but then you loose the distinction between meta-level and object level logic. You want to keep you meta logic simple and separate from your object logic


Last updated: Sep 25 2022 at 23:25 UTC