Yiming Xu (Dec 09 2024 at 07:36): Yiming Xu (Dec 09 2024 at 07:36):I want to use ex_neg_all_pos to refine the following goal:
proof (state)
goal (2 subgoals):
1. ⋀M w. (⋀f1 f2. (f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2) ⟹
length fl1 = length fl2 ⟹
(⋀f1 f2. (f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2) ⟹
length fl1 = length fl2 ⟹
w ∈ world M ⟹
∃vl. length vl = length fl1 ∧ rel M m (w # vl) ∧ (∀x y. (x, y) ∈ set (zip vl fl1) ⟶ asatis M x y) ⟹
w ∈ world M ∧
(∃vl. length vl = length fl2 ∧ rel M m (w # vl) ∧ (∀x y. (x, y) ∈ set (zip vl fl2) ⟶ asatis M x y))
I unfold with ex_neg_all_pos, and want to eliminate the ∃vl. in
∃vl. length vl = length fl1 ∧ rel M m (w # vl) ∧ (∀x y. (x, y) ∈ set (zip vl fl1) ⟶ asatis M x y)
It does not work. How can I get it to work, in the sense of pulling the existential to the very front?
Ideally I want the same effect as rewriting with PULL_EXISTS in HOL4:
PULL_EXISTS;
val it =
⊢ ∀P Q.
((∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q) ∧ ((∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q) ∧
(Q ∧ (∃x. P x) ⇔ ∃x. Q ∧ P x): them
Another example that I want to use ex_neg_all_pos:
proof (prove)
using this:
∃m fl. phi = ♢m fl ∧ m ∈ ops sig ∧ length fl = arity sig m ∧ (∀f. f ∈ set fl ⟶ f ∈ deg_wffs n sig)
?c ∈ quotient' (deg_wffs n sig) (cequivr TYPE('a)) ⟹ f ?c ∈ ?c
goal (1 subgoal):
1. ∃phi0. phi0 ∈ cDIAMs_comb sig (f ` quotient' (deg_wffs n sig) (cequivr TYPE('a))) ∧ cequiv TYPE('a) phi phi0
I want to eliminate ?m fl in
∃m fl. phi = ♢m fl ∧ m ∈ ops sig ∧ length fl = arity sig m ∧ (∀f. f ∈ set fl ⟶ f ∈ deg_wffs n sig)
When I see such a long goal, my reaction is:
1. either auto will solve it with some help (auto + sledgehammer + combining the two tactics in one line). In this case, the question is not really relevant
2. or auto will not work, in which case you want Isar. And in this case, the question is not really relevant either, because you can use obtain.
So, why?
Mathias Fleury (Dec 09 2024 at 08:48):For trying it out, this works:
lemma ‹P ⟹ (∃x. Q x ⟹ H) ›
apply clarify
But again, auto is doing it too
Yiming Xu (Dec 09 2024 at 08:56):Clarify works, thanks and this is what I want. Just discovered that I can do:
proof (intro impI allI iffI,elim conjE, auto) , i.e. use auto without the apply mode.
Mathias Fleury (Dec 09 2024 at 08:56):Yeah but no, do not do that
Mathias Fleury (Dec 09 2024 at 08:56):This is really bad for maintenance
Yiming Xu (Dec 09 2024 at 08:56):So is clarify better?
Mathias Fleury (Dec 09 2024 at 08:56):The output of auto can change across version (or if you later add a simp rule)
Yiming Xu (Dec 09 2024 at 08:57):Or I should just use "obtain" to make it easier for maintenance?
Mathias Fleury (Dec 09 2024 at 08:57):obtain is better
Yiming Xu (Dec 09 2024 at 08:57):Mathias Fleury said:
The output of auto can change across version (or if you later add a simp rule)
How can I add a simp rule that pulling all the existential to the very top?
Mathias Fleury (Dec 09 2024 at 08:58):clarify is useful for exploration (is there a way to get this done fast?)
Yiming Xu (Dec 09 2024 at 08:58):I think I like the aspect of Isar that keeps critical points of proofs clearer, but I am annoyed when I need to use Isar just to treat the logical operations.
Mathias Fleury (Dec 09 2024 at 08:59):Yiming Xu said:
Mathias Fleury said:
The output of auto can change across version (or if you later add a simp rule)
How can I add a simp rule that pulling all the existential to the very top?
The very point of simp rules is that they work for HOL stuff, aka not across ==> (yes there is a Pure.simp, but it is very limited)
Yiming Xu (Dec 09 2024 at 09:00):Not across ==> is very unfortunate...
Yiming Xu (Dec 09 2024 at 09:00):Should not be too hard to get some volunteer implement it. But it would be another story.
Mathias Fleury (Dec 09 2024 at 09:01):Yiming Xu said:
I think I like the aspect of Isar that keeps critical points of proofs clearer, but I am annoyed when I need to use Isar just to treat the logical operations.
why would you? For such a goal, I would:
Mathias Fleury (Dec 09 2024 at 09:02):Especially since the original goal looks like an induction of some sort, using (is _) to name things is not hard at all.
Yiming Xu (Dec 09 2024 at 09:03):I would think an ideal way of using Isar is "only write the steps that tells the real story of the proof". But I will admit that this is my excuse of being lazy.
Yiming Xu (Dec 09 2024 at 09:04):I will learn to live with it. I do use some "is", but often forget that.
Mathias Fleury (Dec 09 2024 at 09:04):Also: you are not using list_induct2 for the prof right?
Yiming Xu (Dec 09 2024 at 09:05):No, but what's the story of list_induct2?
Mathias Fleury (Dec 09 2024 at 09:05):Yiming Xu said:
I will learn to live with it. I do use some "is", but often forget that.
BTW, one trick that I learned after way too long: is _ is _ is _ works
Mathias Fleury (Dec 09 2024 at 09:06):for naming several things at once
Yiming Xu (Dec 09 2024 at 09:06):Ha? What is the syntax?
Mathias Fleury (Dec 09 2024 at 09:06):Yiming Xu said:
No, but what's the story of
list_induct2?
It should just be a better induction principle for what you are trying to do
Yiming Xu (Dec 09 2024 at 09:07):I was not using any sort of induction but this principle sounds sensible. I think I can do a inductive argument using this as well... Let me try.
Mathias Fleury (Dec 09 2024 at 09:08):lemma
assumes ‹((f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2)› (is ‹?P ⟹ ?Q› is ‹_ ∈ ?H ⟹ _›)
shows P
proof -
term ?H
term ?P
term ?Q
Yiming Xu said:
I was not using any sort of induction but this principle sounds sensible. I think I can do a inductive argument using this as well... Let me try.
(⋀f1 f2. (f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2) looks a lot like an induction principle to me
Yiming Xu (Dec 09 2024 at 09:10):Mathias Fleury said:
lemma assumes ‹((f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2)› (is ‹?P ⟹ ?Q› is ‹_ ∈ ?H ⟹ _›) shows P proof - term ?H term ?P term ?Q
I see this is wonderful.
Yiming Xu (Dec 09 2024 at 09:11):Mathias Fleury said:
Yiming Xu said:
I was not using any sort of induction but this principle sounds sensible. I think I can do a inductive argument using this as well... Let me try.
(⋀f1 f2. (f1, f2) ∈ set (zip fl1 fl2) ⟹ ∀M w. asatis M w f1 = asatis M w f2)looks a lot like an induction principle to me
I think you are right, lists sort-of born for an induction.
Last updated: Dec 30 2024 at 16:22 UTC