CODEWITHSUNDEEP
coq
user15163266
user15163266

Reputation: 13

how to proof (f1+f1 = f2+f2 -> f1 = f2) in coq

I'm new to Coq. I want to proof a lemma:

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.

but I dont know how to do it.I have proofed plus comm lemma with ring

Lemma fun_add_comm : forall f g, f +f g = g +f f.
Proof.
intros.
apply functional_extensionality.
intros.
unfold fadd.
ring.
Qed.

but it seems doesnt work in this.

Upvotes: 1

Views: 142

Answers (3)

larsr
larsr

Reputation: 5811

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.

Upvotes: 0

Yves
Yves

Reputation: 4266

With the tactics library that you are using comes an automatic proof extension, called lra. YOu can benefit from it.

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.

It is not easy to recognize that f x + f x is actually (f +f f) x, so you need to help the system by making it explicit in the statement of the assert command.

Upvotes: 1

Pierre Jouvelot
Pierre Jouvelot

Reputation: 923

If you want to do mathematics in CoQ, I suggest you have a look at the SSReflect tactics language, as well as the Mathematical Components libraries (and book, available online).

Here is a proof of your lemma using this framework (there are probably simpler versions).

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.

Note that the =1 equality used here for function equality corresponds to functional extensionality (two functions are equal if their applications to any argument are equal).

Upvotes: 1

Related Questions