更改功能在一個點

Question

我有兩個元素f : X -> bool和x : X。

如何定義g : X -> bool這樣的g x = true和g y = f y對於y！= x。

Answer 1

在回答我的評論之後，我不認爲你可以定義一個「函數」g，因爲你需要一種建設性的方式來區分x與X類型的其他實例。但是，您可以定義兩者之間的關係，如果您獲得可決定性，可以將其轉換爲函數。 喜歡的東西：

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. 

Answer 2

只是補充Vinz的答案，也沒有定義任意X這樣的功能的方式，因爲它意味着X有「幾乎可判定的」平等：

Section Dec. 

Variable X : Type. 

Variable override : (X -> bool) -> X -> X -> bool. 

Hypothesis Hoverride_eq : forall f x, override f x x = true. 
Hypothesis Hoverride_neq : forall f x x', x <> x' -> override f x x' = f x'. 

Lemma xeq_dec' (x x' : X) : {~ x <> x'} + {x <> x'}. 
Proof. 
    destruct (override (fun _ => false) x x') eqn:E. 
    - left. 
    intros contra. 
    assert (H := Hoverride_neq (fun _ => false) _ _ contra). 
    simpl in H. 
    congruence. 
    - right. 
    intros contra. 
    subst x'. 
    rewrite Hoverride_eq in E. 
    discriminate. 
Qed. 

End Dec. 

這引理說如果有一種方法可以做你要求的X，那麼可以測試X的兩個元素x和x'是否相等，除了在中得到的相等證明案件實際上是對x = x'的雙重否定的證明。