Search code examples
coq

Change a function at one point

I have two elements f : X -> bool and x : X.

How to define g : X -> bool such g x = true and g y = f y for y != x.

Solution

  • Following your answer to my comment, I don't think you can define a "function" g, because you need a constructive way do distinguish x from other instances of type X. However you could define a relation between the two, which could be transformed into a function if you get decidability. Something like:

    Parameter X : Type.
Parameter f : X -> bool.
Parameter x : X.

Inductive gRel : X -> bool -> Prop :=
  | is_x : gRel x true
  | is_not_x : forall y: X, y <> x -> gRel y (f y)
.

Definition gdec (h: forall a b: X, {a = b}+{a <> b}) : X -> bool :=
  fun a => if h a x then true else f a.

Lemma gRel_is_a_fun: (forall a b: X, {a = b}+{a <> b}) ->
  exists g : X -> bool, forall a, gRel a (g a).
Proof.
intro hdec.
exists (gdec hdec); unfold gdec.
intro a; destruct (hdec a x).
now subst; apply is_x.
now apply is_not_x.
Qed.