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.

`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))"`

[Thanks to the problem author Max Haslbeck, and the translators Kevin Kappelmann (Lean) and Kathrin Stark (Coq).]

Download Files
### Definitions File

### Template File

### Check 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

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

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

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin type_synonym vname = string definition support :: "((vname ⇒ nat) ⇒ bool) ⇒ vname set" where "support P = {x. ∃s1 s2. (∀y. y ≠ x ⟶ s1 y = s2 y) ∧ P s1 ≠ P s2}" lemma lupd: "x ∉ support Q ⟹ 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

theory Submission imports Defs begin lemma prove: "∀P. (∀s1 s2. (∀i∈support P. s1 i = s2 i) ⟶ P s1 = P s2)" sorry (* OR *) lemma disprove: "~ (∀P. (∀s1 s2. (∀i∈support P. s1 i = s2 i) ⟶ P s1 = P s2))" sorry end

theory Check imports Submission begin lemma "~ (∀P. (∀s1 s2. (∀i∈Defs.support P. s1 i = s2 i) ⟶ P s1 = P s2))" apply(fact Submission.disprove) done (* OR *) lemma " (∀P. (∀s1 s2. (∀i∈Defs.support P. s1 i = s2 i) ⟶ P s1 = P s2))" apply(fact Submission.prove) done end

Download Files
### Definitions File

### Template File

Set Implicit Arguments. Require Export List. Require Export Logic.Decidable Classes.EquivDec. Section Support. Variable vname: Type. Variable vname_dec : EqDec vname eq. Variable vname_infinite : ~ exists xs, forall (x : vname), In x xs. Definition support (P : (vname -> nat) -> Prop) : vname -> Prop := fun x => exists s1 s2, (forall y, y <> x -> s1 y = s2 y) /\ ~ (P s1 <-> P s2). Definition update {X Y: Type} (H : EqDec X eq) (f : X -> Y) (x : X) (n : Y) := fun z => if (H z x) then n else f z. (** Do you need this lemma somewhere? - I didnt. Otherwise we could delete it. *) Lemma lupd x Q (dec_Q: forall x y, (Q x <-> Q y) \/ ~ (Q x <-> Q y)): ~ support Q x -> (forall l n, Q (update vname_dec l x n) <-> Q l). Proof. intros. unfold update, support in *. destruct (dec_Q (update vname_dec l x n) l); eauto. enough (exists s1 s2 : vname -> nat, (forall y : vname, y <> x -> s1 y = s2 y) /\ ~ (Q s1 <-> Q s2)) as (?&?&?&?); [firstorder|]. - exists (fun z : vname => if vname_dec z x then n else l z). exists l. split; eauto. intros. destruct (vname_dec y x); congruence. Qed. (** Definition of finite in Coq. As Coq has not such a big focus on sets etc we prove the statements ourselves. *) Definition finite (f : vname -> Prop) : Prop := exists xs, forall x, f x -> In x xs. Lemma finite_false (f : vname -> Prop): (forall x, f x -> False) -> finite f. Proof. exists nil. intros x A. firstorder. Qed. Lemma infinite_true (f: vname -> Prop): (forall x, f x) -> ~ finite f. Proof. intros H (xs&H'). apply vname_infinite. eauto. Qed. (** Definition of const *) Definition const (n : nat) := fun (x : vname) => n. End Support.

Require Import Defs. Section Support. Variable vname: Type. Variable vname_dec : EqDec vname eq. Variable vname_infinite : ~ exists xs, forall (x : vname), In x xs. Lemma decidable_prop : decidable (forall P s1 s2, (forall (i: vname), support P i -> s1 i = s2 i) -> P s1 = P s2 ). Proof. Admitted. End Support.

Download Files
### Definitions File

### Template File

### Check File

-- Lean version: 3.4.2 -- Mathlib version: 2019-07-31 import tactic.push_neg import tactic.rcases def support (P : (string → ℕ) → Prop) : set string := { a | ∃ (s1 s2 : string → ℕ), (∀ a', a' ≠ a → s1 a' = s2 a') ∧ P s1 ≠ P s2 } /-- Given a function `f : string → ℕ`, `(a a' : string)`, and `b : ℕ`, `(subst f a b) a'` returns `b` if `a' = a` and `f a'` otherwise. -/ @[simp] noncomputable def subst (f : string → ℕ) (a : string) (b : ℕ) := (λ a', if a' = a then b else f a') -- `↦` can be typed by `\mapsto` notation f `[`a` ↦ `b`]` := subst f a b lemma xams_lemma (P : (string → ℕ) → Prop) {a : string} : a ∉ support P → (∀ s b, P (s[a ↦ b]) = P s) := begin assume (hyp : a ∉ support P) s b, change ¬∃ (s1 s2 : string → ℕ), (∀ (a' : string), a' ≠ a → s1 a' = s2 a') ∧ P s1 ≠ P s2 at hyp, replace hyp : ∀ (s1 s2 : string → ℕ), (∃ (a' : string), a' ≠ a ∧ s1 a' ≠ s2 a') ∨ P s1 = P s2, by { push_neg at hyp, exact hyp }, have : (∃ (a' : string), a' ≠ a ∧ s[a ↦ b] a' ≠ s a') ∨ P (s[a ↦ b]) = P s, from hyp (s[a ↦ b]) s, cases this, { rcases this with ⟨a', a'_ne_a, _⟩, have : s[a ↦ b] a' = s a', by simp [a'_ne_a], contradiction }, { assumption } end

import .defs -- prove one of the following lemmas lemma prove : ∀ (P : (string → ℕ) → Prop) (s1 s2 : string → ℕ) (a ∈ support P), s1 a = s2 a → P s1 = P s2 := sorry lemma disprove: ¬∀ (P : (string → ℕ) → Prop) (s1 s2 : string → ℕ) (a ∈ support P), s1 a = s2 a → P s1 = P s2 := sorry

import .defs import .submission -- prove one of the following lemmas lemma goal : ∀ (P : (string → ℕ) → Prop) (s1 s2 : string → ℕ) (a ∈ support P), s1 a = s2 a → P s1 = P s2 := prove -- OR lemma goal : ¬∀ (P : (string → ℕ) → Prop) (s1 s2 : string → ℕ) (a ∈ support P), s1 a = s2 a → P s1 = P s2 := disprove

Terms and Conditions