如何在coq中证明(f1+f1 = f2+f2 -> f1 = f2)
如何在coq中证明(f1+f1 = f2+f2 -> f1 = f2)
提问于 2021-02-08 00:28:57
我是Coq的新手。我想证明一个引理：
Require Import Reals.
Open Scope R_scope.
Definition fadd (f g:R->R) := fun x => f x + g x.
Notation "f +f g" := (fadd f g) (at level 61, left associativity).
(** f+f = g+g->f=g **)
Lemma fun_add: forall f g, f +f f = g +f g -> f = g.但是我不知道怎么做。我已经证明了加环的通信引理
Lemma fun_add_comm : forall f g, f +f g = g +f f.
Proof.
intros.
apply functional_extensionality.
intros.
unfold fadd.
ring.
Qed.但它似乎不能在这里工作。
回答 3
Stack Overflow用户
回答已采纳
发布于 2021-02-08 02:28:26
如果你想用CoQ做数学，我建议你看一看SSReflect策略语言，以及数学组件库(还有书，可用的online)。
这是你的引理使用这个框架的一个证明(可能还有更简单的版本)。
From Coq Require Import Init.Prelude Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
Require Import Reals.
Open Scope R_scope.
Definition fadd (f g:R->R) := fun x => f x + g x.
Notation "f +f g" := (fadd f g) (at level 61, left associativity).
Lemma fun_add: forall f g, f +f f =1 g +f g -> f =1 g.
Proof.
move=> f g eq2f2g x.
move: (eq2f2g x).
rewrite /fadd -!double => eq2fx2gx.
by apply: (Rmult_eq_reg_l 2).
Qed.请注意，这里用于函数相等的=1相等对应于函数的可扩展性(如果两个函数对任何参数的应用相等，则它们是相等的)。
Stack Overflow用户
发布于 2021-02-08 19:59:14
您正在使用的策略库附带了一个名为lra的自动证明扩展。YOu可以从中受益。
Require Import FunctionalExtensionality.
Require Import Reals Lra.
Definition fadd (f g:R->R) := fun x => f x + g x.
Notation "f +f g" := (fadd f g) (at level 61, left associativity).
Lemma fun_add: forall f g, f +f f = g +f g -> f = g.
Proof.
intros f g adds.
apply functional_extensionality.
intros x.
assert (adds_on_x : (f +f f) x = (g +f g) x).
rewrite adds.
reflexivity.
unfold fadd in adds_on_x.
lra.
Qed.要识别出f x + f x实际上是(f +f f) x并非易事，因此您需要在assert命令的语句中明确地说明这一点，以帮助系统。
Stack Overflow用户
发布于 2021-02-09 17:42:18
Require Import Reals Lra.
Notation "f =1 g" := (forall x, f x = g x) (at level 80).
Notation "f +' g" := (fun x => f x + g x)%R (at level 61).
Goal forall (f g : R -> R), f +' f =1 g +' g -> f =1 g.
intros f g H x.
pose proof (H x) as Hx.
lra.
Qed.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/66090237
复制相关文章
相似问题
腾讯云开发者
