Stream: Beginner Questions

Topic: Question about fun extends to linorder


view this post on Zulip Hongjian Jiang (Jul 31 2023 at 17:58):

By looking for the order.thy, I find the instance instance "fun" :: (type, order) order proof qed (auto simp add: le_fun_def intro: order.antisym). There is a straight idea whether fun could extend to linorder too.

Any help would be appreciated.

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 19:16):

if could give idea to solve below lemma proving would be better

datatype 'a rexp =
  is_Zero: Zero |
  is_One: One |
  Sym "'a Predicate.pred"|
  Plus "('a rexp)" "('a rexp)" |
  Times "('a rexp)" "('a rexp)" |
  Star "('a rexp)"


instantiation rexp :: (order) "{order}"
begin

fun le_rexp :: "('a::order) rexp ⇒ ('a::order) rexp ⇒ bool"
where
  "le_rexp Zero _ = True"
| "le_rexp _ Zero = False"
| "le_rexp One _ = True"
| "le_rexp _ One = False"
| "le_rexp (Sym a) (Sym b) = (Predicate.eval a ≤ Predicate.eval b)"
| "le_rexp (Sym _) _ = True"
| "le_rexp _ (Sym _) = False"
| "le_rexp (Star r) (Star s) = le_rexp r s"
| "le_rexp (Star _) _ = True"
| "le_rexp _ (Star _) = False"
| "le_rexp (Plus r r') (Plus s s') =
    (if r = s then le_rexp r' s' else le_rexp r s)"
| "le_rexp (Plus _ _) _ = True"
| "le_rexp _ (Plus _ _) = False"
| "le_rexp (Times r r') (Times s s') =
    (if r = s then le_rexp r' s' else le_rexp r s)"

term "Predicate.eval a"

definition less_eq_rexp where "r ≤ s ≡ le_rexp r s"
definition less_rexp where "r < s ≡ le_rexp r s ∧ r ≠ s"

lemma le_rexp_Zero: "le_rexp r Zero ⟹ r = Zero"
by (induction r) auto

lemma le_rexp_refl: "le_rexp r r"
by (induction r) auto

lemma le_rexp_antisym: "⟦le_rexp r s; le_rexp s r⟧ ⟹ r = s"
  apply(induction r s rule: le_rexp.induct)
                      apply auto
  using le_rexp_Zero apply auto[1]
  by (simp add: pred.expand)

lemma le_rexp_trans: "⟦le_rexp r s; le_rexp s t⟧ ⟹ le_rexp r t"
proof (induction r s arbitrary: t rule: le_rexp.induct)
  fix v t assume "le_rexp (Sym v) t" thus "le_rexp One t" by (cases t) auto
next
  fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto
next
  fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto
next
  fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto
next
  fix v u t assume "le_rexp (Sym v) (Sym u)" "le_rexp (Sym u) t"
  thus "le_rexp (Sym v) t" by (cases t) auto
next
  fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
  fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
  fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
  fix r s t
  assume IH: "⋀t. le_rexp r s ⟹ le_rexp s t ⟹ le_rexp r t"
    and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t"
  thus "le_rexp (Star r) t" by (cases t) auto
next
  fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
next
  fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
next
  fix r1 r2 s1 s2 t
  assume "⋀t. r1 = s1 ⟹ le_rexp r2 s2 ⟹ le_rexp s2 t ⟹ le_rexp r2 t"
         "⋀t. r1 ≠ s1 ⟹ le_rexp r1 s1 ⟹ le_rexp s1 t ⟹ le_rexp r1 t"
         "le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t"
  thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
next
  fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto
next
  fix r1 r2 s1 s2 t
  assume "⋀t. r1 = s1 ⟹ le_rexp r2 s2 ⟹ le_rexp s2 t ⟹ le_rexp r2 t"
         "⋀t. r1 ≠ s1 ⟹ le_rexp r1 s1 ⟹ le_rexp s1 t ⟹ le_rexp r1 t"
         "le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t"
  thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
qed auto

instance proof
qed (auto simp add: less_eq_rexp_def less_rexp_def
       intro: le_rexp_refl le_rexp_antisym le_rexp_trans)

end

instantiation rexp :: (linorder) "{linorder}"
begin

lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s ∨ le_rexp s r"
  apply (induction r s rule: le_rexp.induct)
  apply auto
  sorry

instance proof
qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total)

end

How to prove the rexp is an instantiation of linorder.

view this post on Zulip Mathias Fleury (Jul 31 2023 at 19:35):

Can you explain to the intuition why you would always have a <= b \/ b < a (in order to have Sym a <= Sym b)?

view this post on Zulip Mathias Fleury (Jul 31 2023 at 19:36):

because that seems far from obvious to me

view this post on Zulip Mathias Fleury (Jul 31 2023 at 19:38):

My intuition is that if you take a = (%x. even x) and b = (%x. prime x), you are going to have a hard timing finding whether a or b is larger…

view this post on Zulip Mathias Fleury (Jul 31 2023 at 19:39):

but maybe I am missing something in your definition

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 19:49):

I am trying to prove the predicate existing relationship of the linorder.

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 19:50):

In such a case, I think a might be equal to b, according to the predicate.eval

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 19:52):

I am not very clear about the relation between the order and linorder. Because like (<) in nat is an order, a < b then a < b or b < a will be always established.

view this post on Zulip Mathias Fleury (Jul 31 2023 at 19:57):

you have a linorder on 'a, that does not say anything on having an order on a function

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:01):

so the question should be recalled back to prove the linorder relation of predicate, whether I could understand in this way

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:02):

No, the question is: what do you want to prove

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:02):

and what you want to model

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:02):

and how

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:05):

in general, total orders on base elements does not mean anything on a function on those elements

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:05):

even with lattices, you only get a partial order

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:07):

okay, I want to implement a symbolic automaton, in which transition is the predicate, thus I include the predicate in the rexp(Sym). And I built on the basic of regular set in afp. When the type of character is nat, it belongs to the linear order. Currently, My theory could not handle such case, that's why I want to prove its linorder.

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:08):

the original library is built on atom 'a, then linear order holds on

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:09):

I see the predicate is a complete-lattices, but not linorder.

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:14):

Wait let's go a step back before going onto the Isabelle part: what does it mean for an automata to have a total order?

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:16):

or do you want to express the subset relationship on the recognized languages?

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:16):

I use the method of derivative on regular expression

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:18):

and it must be built on normal forms, and need some arbitrary total order on regular expressions

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:20):

The relation \le can be some arbitrary total order on regular expressions. Our concrete definition (omitted) works as follows. Expressions with different constructors at the root are compared according to some arbitrary fixed total order of the constructors. Expressions with the same constructor at the root are compared according to the lexicographic order of the arguments. Atoms are assumed to be totally ordered. More precisely,  \le is restricted to regular expressions over natural numbers. cite Proof Pearl: Regular Expression Equivalence and Relation Algebra

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:27):

if you just need a total order, I think that you could ignore most of the Sym problem… something like Sym a < Sym b iff a 0 < b 0

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:28):

but I am not sure at the moment.

view this post on Zulip Mathias Fleury (Jul 31 2023 at 20:28):

what you do not want is working on the function as a function to build an order

view this post on Zulip Hongjian Jiang (Jul 31 2023 at 20:33):

Sorry, not understand the final sentence, not very familiar with the function on order.

Why I need a total order or linear order lies on I could verify the bool value, but not for the nat value. So I guess the problem lies on the rexp doesn't support linear. If available, I could email you the project and see where is the problem on.


Last updated: Feb 27 2024 at 08:17 UTC