Variables

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

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

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

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

Download Files

Definitions 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.

Template File

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

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

Template File

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

Check File

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

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

Cookies disclaimer

Variables

Resources

Definitions File

Template File

Check File

Definitions File

Template File

Check File

Definitions File

Template File

Definitions File

Template File

Check File

Definitions File

Template File

Check File