Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Variable

Xam was working on some functions that took a state and returned some result. He wondered how he could alter the states while not altering the result of these functions. The first idea that came to his mind was to define the set of variables that the function would depend on. He called it the support of function P:

support P = {x. ∃ s1 s2. ( ∀ y. y ≠ x --> s1 y = s2 y) ∧ P s1 ≠ P s2}

He was really happy, when he could show, that altering a variable not in the support of some function doesnt alter the function.

x ∉ support Q ==> Q (l(x:=n)) = Q l

But that was not quite what he wanted. He rather was looking for something else: He wanted to prove that for two states that agree on the support of a function, the function's result for the two states would be equal.
As the lunch break interupted him, he had no more time to think about it. While having coffee he thus posted the question to his fellows, who could not immediately come up with a solution. Could you?

Prove or disprove:

∀ P. (∀s1 s2. ( ∀ i∈support P. s1 i = s2 i) ==> P s1 = P s2)

~ ( ∀ P. ( ∀ s1 s2. ( ∀ i∈support P. s1 i = s2 i) ==> P s1 = P s2))"


Resources

Download Files

Definitions File

theory Defs
  imports Main  
begin

type_synonym vname = string

definition support :: "((vname \<Rightarrow> nat) \<Rightarrow> bool) \<Rightarrow> vname set" where
"support P = {x. \<exists>s1 s2. (\<forall>y. y \<noteq> x \<longrightarrow> s1 y = s2 y) \<and> P s1 \<noteq> P s2}"


lemma lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l"
by(simp add: support_def fun_upd_other fun_eq_iff)
  (metis (no_types, lifting) fun_upd_def)
   
  
end

Template File

theory Submission
  imports Defs
begin
  
lemma prove: "\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2)"
sorry

(* OR *)
 
lemma disprove: "~ (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))"
sorry

end

Check File

theory Check
imports Submission
begin
 
lemma "~ (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>Defs.support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))"
apply(fact Submission.disprove) done
(* OR *)

lemma " (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>Defs.support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))"
apply(fact Submission.prove) done

end

Terms and Conditions