Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl. Style: centered; floating; windowed.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From Coq Require Import FunctionalExtensionality. From stdpp Require Import prelude finite. From VLSM.Lib Require Import Preamble StdppExtras ListExtras FinSetExtras.

Utility: Finitely Supported Functions

The support of a function (w.r.t. a specified codomain value) is the type of elements of its domain that are not mapped to the specified value.
Note that we require the codomain to have decidable equality, because it allows for a straight-forward approach to proving equality of elements of the support.
Definition support {A B : Type} (s : B) (f : A -> B) `{EqDecision B} : Type :=
  dsig (fun a => f a <> s).
A function is finitely supported if its support is Finite. We define a type to encapsulate functions of finite support.
Definition fsfun (A : Type) `(s : B) `{EqDecision A, EqDecision B} : Type :=
  {f : A -> B & Finite (support s f)}.

Definition fsfun_project
  {A B : Type} {b : B} `{EqDecision A, EqDecision B} : fsfun A b -> A -> B :=
  projT1.

Coercion fsfun_project : fsfun >-> Funclass.

#[global] Arguments fsfun_project : simpl never.

Section sec_fsfun_fixed_domain.

Context
  `{EqDecision A}
  .

Section sec_fsfun_fixed_supp_value.

Context
  `{EqDecision B}
  {b : B}
  .

#[export] Instance fsfun_equiv : Equiv (fsfun A b) :=
  fun f g => fsfun_project f = fsfun_project g.

A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Equivalence equiv
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Equivalence equiv
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Equivalence (λ f g : fsfun A b, f = g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Symmetric (λ f g : fsfun A b, f = g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
Transitive (λ f g : fsfun A b, f = g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Symmetric (λ f g : fsfun A b, f = g)
by intros f g; apply symmetry.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Transitive (λ f g : fsfun A b, f = g)
by intros f g h; apply transitivity. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq) fsfun_project
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq) fsfun_project
by intros f g Heqv; inversion Heqv. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq) projT1
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq) projT1
by apply fsfun_project_proper. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b

f ≡ g ↔ f = g
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b

f ≡ g ↔ f = g
done. Qed. #[export] Instance fsfun_has_fin_supp (f : fsfun A b) : Finite (support b f) := projT2 f. Definition fin_supp (f : fsfun A b) : list A := map proj1_sig (enum (support b f)).
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

a : A, a ∈ fin_supp f ↔ f a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

a : A, a ∈ fin_supp f ↔ f a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

a : A, a ∈ map proj1_sig (enum (support b f)) ↔ f a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A

( y : {x : A | bool_decide (f x ≠ b)}, a = `y ∧ y ∈ enum (support b f)) → f a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A
f a ≠ b → y : {x : A | bool_decide (f x ≠ b)}, a = `y ∧ y ∈ enum (support b f)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A

( y : {x : A | bool_decide (f x ≠ b)}, a = `y ∧ y ∈ enum (support b f)) → f a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
asupp: {x : A | bool_decide (f x ≠ b)}

f (`asupp) ≠ b
by destruct_dec_sig asupp _a H_a Heq; subst.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A

f a ≠ b → y : {x : A | bool_decide (f x ≠ b)}, a = `y ∧ y ∈ enum (support b f)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A
Ha: f a ≠ b

y : {x : A | bool_decide (f x ≠ b)}, a = `y ∧ y ∈ enum (support b f)
by exists (dexist a Ha); split; [| apply elem_of_enum]. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

a : A, a ∉ fin_supp f ↔ f a = b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

a : A, a ∉ fin_supp f ↔ f a = b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A

¬ f a ≠ b ↔ f a = b
by destruct (decide (f a = b)); itauto. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

NoDup (fin_supp f)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

NoDup (fin_supp f)
by apply dsig_NoDup_map, NoDup_enum. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> Permutation) fin_supp
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> Permutation) fin_supp
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heq: f ≡ g

fin_supp f ≡ₚ fin_supp g
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heq: f ≡ g

x : A, x ∈ fin_supp f ↔ x ∈ fin_supp g
by intro; rewrite !elem_of_fin_supp, Heq. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

RelDecision equiv
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

RelDecision equiv
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b

Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Hneqv: list_to_set (fin_supp f) ≢ list_to_set (fin_supp g)

Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Hneqv: list_to_set (fin_supp f) ≢ list_to_set (fin_supp g)

Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Hneqv: list_to_set (fin_supp f) ≢ list_to_set (fin_supp g)
Heqv: f ≡ g

False
by rewrite Heqv in Hneqv.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)

Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Hall: set_Forall (λ a : A, f a = g a) (list_to_set (fin_supp f))

Decision (f ≡ g)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Hall: set_Forall (λ a : A, f a = g a) (list_to_set (fin_supp f))
a: A

f a = g a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Hall: set_Forall (λ a : A, f a = g a) (list_to_set (fin_supp f))
a: A
Hf: a ∉ fin_supp f

f a = g a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Hall: set_Forall (λ a : A, f a = g a) (list_to_set (fin_supp f))
a: A
Hf: a ∉ fin_supp f
Hg: a ∉ fin_supp g

f a = g a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: list_to_set (fin_supp f) ≡ list_to_set (fin_supp g)
Hall: set_Forall (λ a : A, f a = g a) (list_to_set (fin_supp f))
a: A
Hf: f a = b
Hg: g a = b

f a = g a
by transitivity b. Qed. Program Definition empty_fsfun : fsfun A b := existT (const b) {| enum := [] |}.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

NoDup []
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

NoDup []
by constructor. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

x : support b (const b), x ∈ []
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

x : support b (const b), x ∈ []
by intros; destruct_dec_sig x a Ha Heq; contradiction Ha. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

fin_supp empty_fsfun = []
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

fin_supp empty_fsfun = []
done. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

fin_supp f = [] → f ≡ empty_fsfun
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b

fin_supp f = [] → f ≡ empty_fsfun
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
Hf: fin_supp f = []
a: A

f a = empty_fsfun a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
Hf: fin_supp f = []
a: A

a ∉ fin_supp f
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
Hf: fin_supp f = []
a: A

a ∉ []
by apply not_elem_of_nil. Qed. Definition update_supp (f : fsfun A b) (n : A) (b' : B) : listset A := if decide (b' = b) then list_to_set (fin_supp f) ∖ {[n]} else {[n]} ∪ list_to_set (fin_supp f).
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

Forall (λ a : A, update f n b' a ≠ b) (elements (update_supp f n b'))
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

Forall (λ a : A, update f n b' a ≠ b) (elements (update_supp f n b'))
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

Forall (λ a : A, update f n b' a ≠ b) (elements (if decide (b' = b) then list_to_set (fin_supp f) ∖ {[n]} else {[n]} ∪ list_to_set (fin_supp f)))
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A

a ∈ elements (if decide (b' = b) then list_to_set (fin_supp f) ∖ {[n]} else {[n]} ∪ list_to_set (fin_supp f)) → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A

a ∈ (if decide (b' = b) then list_to_set (fin_supp f) ∖ {[n]} else {[n]} ∪ list_to_set (fin_supp f)) → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = b

a ∈ list_to_set (fin_supp f) ∖ {[n]} → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ b
a ∈ {[n]} ∪ list_to_set (fin_supp f) → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = b

a ∈ list_to_set (fin_supp f) ∖ {[n]} → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = b

f a ≠ b ∧ a ≠ n → update f n b' a ≠ b
by intros []; rewrite update_neq.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ b

a ∈ {[n]} ∪ list_to_set (fin_supp f) → update f n b' a ≠ b
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ b

a = n ∨ f a ≠ b → update f n b' a ≠ b
by unfold update; case_decide; cbn; intros []. Qed. Program Definition update_fsfun (f : fsfun A b) (n : A) (b' : B) : fsfun A b := existT (update f n b') {| enum := list_annotate (update_supp_all f n b') |}.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

(f : fsfun A b) (n : A) (b' : B), NoDup (list_annotate (update_supp_all f n b'))
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

(f : fsfun A b) (n : A) (b' : B), NoDup (list_annotate (update_supp_all f n b'))
by intros; apply list_annotate_NoDup, NoDup_elements. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

(f : fsfun A b) (n : A) (b' : B) (x : support b (update f n b')), x ∈ list_annotate (update_supp_all f n b')
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

(f : fsfun A b) (n : A) (b' : B) (x : support b (update f n b')), x ∈ list_annotate (update_supp_all f n b')
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b

dexist a Ha ∈ list_annotate (update_supp_all f n b')
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b

`(dexist a Ha) ∈ update_supp f n b'
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' = b

`(dexist a Ha) ∈ list_to_set (fin_supp f) ∖ {[n]}
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' ≠ b
`(dexist a Ha) ∈ {[n]} ∪ list_to_set (fin_supp f)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' = b

`(dexist a Ha) ∈ list_to_set (fin_supp f) ∖ {[n]}
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' = b

f a ≠ b ∧ a ≠ n
by unfold update in Ha; case_decide; split; congruence.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' ≠ b

`(dexist a Ha) ∈ {[n]} ∪ list_to_set (fin_supp f)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
Ha: update f n b' a ≠ b
H: b' ≠ b

a = n ∨ f a ≠ b
by unfold update in Ha; case_decide; [left | right]. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

update_fsfun f n b' n = b'
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

update_fsfun f n b' n = b'
by setoid_rewrite update_eq. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

m : A, m ≠ n → update_fsfun f n b' m = f m
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

m : A, m ≠ n → update_fsfun f n b' m = f m
by intros; setoid_rewrite update_neq. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq ==> eq ==> equiv) update_fsfun
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B

Proper (equiv ==> eq ==> eq ==> equiv) update_fsfun
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
n: A
b': B

update_fsfun f n b' ≡ update_fsfun g n b'
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
n: A
b': B
a: A

update_fsfun f n b' a = update_fsfun g n b' a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
b': B
a: A

update_fsfun f a b' a = update_fsfun g a b' a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
n: A
b': B
a: A
n0: n ≠ a
update_fsfun f n b' a = update_fsfun g n b' a
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
b': B
a: A

update_fsfun f a b' a = update_fsfun g a b' a
by rewrite !update_fsfun_eq.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
n: A
b': B
a: A
n0: n ≠ a

update_fsfun f n b' a = update_fsfun g n b' a
by rewrite !update_fsfun_neq, Heqv. Qed.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

a : A, a ∈ fin_supp (update_fsfun f n b') ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B

a : A, a ∈ fin_supp (update_fsfun f n b') ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A

a ∈ map proj1_sig (list_annotate (update_supp_all f n b')) ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A

a ∈ update_supp f n b' ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = b

a ∈ list_to_set (fin_supp f) ∖ {[n]} ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ b
a ∈ {[n]} ∪ list_to_set (fin_supp f) ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = b

a ∈ list_to_set (fin_supp f) ∖ {[n]} ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
by rewrite elem_of_difference, elem_of_list_to_set, elem_of_singleton; split; itauto.
A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ b

a ∈ {[n]} ∪ list_to_set (fin_supp f) ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
by rewrite elem_of_union, elem_of_list_to_set, elem_of_singleton; split; itauto. Qed. End sec_fsfun_fixed_supp_value.

Finitely supported functions on naturals

Definition zero_fsfun : fsfun A 0 := empty_fsfun.

A: Type
EqDecision0: EqDecision A

n : A, zero_fsfun n = 0
A: Type
EqDecision0: EqDecision A

n : A, zero_fsfun n = 0
done. Qed. Definition succ_fsfun (f : fsfun A 0) (n : A) : fsfun A 0 := update_fsfun f n (S (f n)).
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

succ_fsfun f n n = S (f n)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

succ_fsfun f n n = S (f n)
by apply update_fsfun_eq. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

m : A, m ≠ n → succ_fsfun f n m = f m
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

m : A, m ≠ n → succ_fsfun f n m = f m
by apply update_fsfun_neq. Qed.
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> eq ==> equiv) succ_fsfun
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> eq ==> equiv) succ_fsfun
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g
n: A

succ_fsfun f n ≡ succ_fsfun g n
by apply update_fsfun_proper; [.. | rewrite Heqv]. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

a : A, a ∈ fin_supp (succ_fsfun f n) ↔ a = n ∨ a ∈ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

a : A, a ∈ fin_supp (succ_fsfun f n) ↔ a = n ∨ a ∈ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A

a ∈ fin_supp (update_fsfun f n (S (f n))) ↔ a = n ∨ a ∈ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A

S (f n) = 0 ∧ a ∈ fin_supp f ∧ a ≠ n ∨ S (f n) ≠ 0 ∧ (a ∈ fin_supp f ∨ a = n) ↔ a = n ∨ a ∈ fin_supp f
by split; itauto lia. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

n ∈ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

n ∈ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp f

fin_supp (succ_fsfun f n) ≡ₚ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp f
x: A

x ∈ fin_supp (succ_fsfun f n) ↔ x ∈ fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp f
x: A

x = n ∨ x ∈ fin_supp f ↔ x ∈ fin_supp f
by set_solver. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

n ∉ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ n :: fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

n ∉ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ n :: fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∉ fin_supp f

elements (update_supp f n (S (f n))) ≡ₚ n :: fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∉ fin_supp f

elements ({[n]} ∪ list_to_set (fin_supp f)) ≡ₚ n :: fin_supp f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∉ fin_supp f

n :: elements (list_to_set (fin_supp f)) ≡ₚ n :: fin_supp f
by constructor; eapply @elements_list_to_set; [typeclasses eauto | apply fin_supp_NoDup]. Qed. Definition delta_nat_fsfun (n : A) : fsfun A 0 := succ_fsfun zero_fsfun n.
A: Type
EqDecision0: EqDecision A
n: A

delta_nat_fsfun n n = 1
A: Type
EqDecision0: EqDecision A
n: A

delta_nat_fsfun n n = 1
by apply succ_fsfun_eq. Qed.
A: Type
EqDecision0: EqDecision A
n: A

m : A, m ≠ n → delta_nat_fsfun n m = 0
A: Type
EqDecision0: EqDecision A
n: A

m : A, m ≠ n → delta_nat_fsfun n m = 0
by apply succ_fsfun_neq. Qed.
A: Type
EqDecision0: EqDecision A
n: A

a : A, a ∈ fin_supp (delta_nat_fsfun n) ↔ a = n
A: Type
EqDecision0: EqDecision A
n: A

a : A, a ∈ fin_supp (delta_nat_fsfun n) ↔ a = n
A: Type
EqDecision0: EqDecision A
n, a: A

a ∈ fin_supp (delta_nat_fsfun n) ↔ a = n
A: Type
EqDecision0: EqDecision A
n, a: A

a ∈ fin_supp (succ_fsfun zero_fsfun n) ↔ a = n
A: Type
EqDecision0: EqDecision A
n, a: A

a = n ∨ False ↔ a = n
by itauto. Qed. Definition fsfun_sum (f : fsfun A 0) : nat := sum_list_with f (fin_supp f).
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> eq) fsfun_sum
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> eq) fsfun_sum
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g

fsfun_sum f = fsfun_sum g
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g

sum_list_with f (fin_supp f) = sum_list_with g (fin_supp g)
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g

sum_list_with f (fin_supp g) = sum_list_with g (fin_supp g)
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g
fin_supp f ≡ₚ fin_supp g
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g

sum_list_with f (fin_supp g) = sum_list_with g (fin_supp g)
by apply sum_list_with_ext_forall; intros; rewrite Heqv.
A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g

fin_supp f ≡ₚ fin_supp g
by apply fin_supp_proper. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0

fsfun_sum f = 0 → f ≡ zero_fsfun
A: Type
EqDecision0: EqDecision A
f: fsfun A 0

fsfun_sum f = 0 → f ≡ zero_fsfun
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: i : A, i ∈ fin_supp f → f i = 0

f ≡ zero_fsfun
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: i : A, i ∈ fin_supp f → f i = 0
a: A

f a = zero_fsfun a
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: i : A, i ∈ fin_supp f → f i = 0
a: A
Ha: f a ≠ zero_fsfun a

False
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: i : A, i ∈ fin_supp f → f i = 0
a: A
Ha: f a ≠ zero_fsfun a
Ha': a ∈ fin_supp f

False
by apply Hall in Ha'. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

fsfun_sum (succ_fsfun f n) = S (fsfun_sum f)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

fsfun_sum (succ_fsfun f n) = S (fsfun_sum f)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

sum_list_with (succ_fsfun f n) (fin_supp (succ_fsfun f n)) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
e: n ∈ fin_supp f

sum_list_with (succ_fsfun f n) (fin_supp (succ_fsfun f n)) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f
sum_list_with (succ_fsfun f n) (fin_supp (succ_fsfun f n)) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
e: n ∈ fin_supp f

sum_list_with (succ_fsfun f n) (fin_supp (succ_fsfun f n)) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
e: n ∈ fin_supp f

sum_list_with (succ_fsfun f n) (fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
e: n ∈ fin_supp f
Hnodup: NoDup (fin_supp f)

sum_list_with (succ_fsfun f n) (fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A

NoDup (fin_supp f) → n ∈ fin_supp f → sum_list_with (succ_fsfun f n) (fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)

NoDup (a :: l) → n ∈ a :: l → sum_list_with (succ_fsfun f n) (a :: l) = S (sum_list_with f (a :: l))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)

(a ∉ l) ∧ NoDup l → n = a ∨ n ∈ l → succ_fsfun f n a + sum_list_with (succ_fsfun f n) l = S (f a + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: n ∉ l
Hnodup: NoDup l

succ_fsfun f n n + sum_list_with (succ_fsfun f n) l = S (f n + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l
succ_fsfun f n a + sum_list_with (succ_fsfun f n) l = S (f a + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: n ∉ l
Hnodup: NoDup l

succ_fsfun f n n + sum_list_with (succ_fsfun f n) l = S (f n + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: n ∉ l
Hnodup: NoDup l

S (f n + sum_list_with (succ_fsfun f n) l) = S (f n + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: n ∉ l
Hnodup: NoDup l

sum_list_with (succ_fsfun f n) l = sum_list_with f l
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: n ∉ l
Hnodup: NoDup l

i : A, i ∈ l → succ_fsfun f n i = f i
by intros; rewrite succ_fsfun_neq by set_solver.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l

succ_fsfun f n a + sum_list_with (succ_fsfun f n) l = S (f a + sum_list_with f l)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: A
l: list A
IHl: NoDup l → n ∈ l → sum_list_with (succ_fsfun f n) l = S (sum_list_with f l)
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l

f a + sum_list_with (succ_fsfun f n) l = S (f a + sum_list_with f l)
by rewrite IHl.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

sum_list_with (succ_fsfun f n) (fin_supp (succ_fsfun f n)) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

sum_list_with (succ_fsfun f n) (n :: fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

S (f n) + sum_list_with (succ_fsfun f n) (fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

1 + sum_list_with (succ_fsfun f n) (fin_supp f) = S (sum_list_with f (fin_supp f))
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

sum_list_with (succ_fsfun f n) (fin_supp f) = sum_list_with f (fin_supp f)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
n0: n ∉ fin_supp f

i : A, i ∈ fin_supp f → succ_fsfun f n i = f i
by intros; rewrite succ_fsfun_neq; [| set_solver]. Qed.
The component-wise sum of two functions
Definition add_fsfun_supp (f1 f2 : fsfun A 0) : listset A :=
  list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2).

A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

Forall (λ a : A, f1 a + f2 a ≠ 0) (elements (add_fsfun_supp f1 f2))
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

Forall (λ a : A, f1 a + f2 a ≠ 0) (elements (add_fsfun_supp f1 f2))
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

a ∈ elements (list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2)) → f1 a + f2 a ≠ 0
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

f1 a ≠ 0 ∨ f2 a ≠ 0 → f1 a + f2 a ≠ 0
by lia. Qed. Program Definition add_fsfun (f1 f2 : fsfun A 0) : fsfun A 0 := existT (fun a => f1 a + f2 a) {| enum := list_annotate (add_fsfun_supp_all f1 f2) |}.
A: Type
EqDecision0: EqDecision A

f1 f2 : fsfun A 0, NoDup (list_annotate (add_fsfun_supp_all f1 f2))
A: Type
EqDecision0: EqDecision A

f1 f2 : fsfun A 0, NoDup (list_annotate (add_fsfun_supp_all f1 f2))
by intros; apply list_annotate_NoDup, NoDup_elements. Qed.
A: Type
EqDecision0: EqDecision A

(f1 f2 : fsfun A 0) (x : support 0 (λ a : A, f1 a + f2 a)), x ∈ list_annotate (add_fsfun_supp_all f1 f2)
A: Type
EqDecision0: EqDecision A

(f1 f2 : fsfun A 0) (x : support 0 (λ a : A, f1 a + f2 a)), x ∈ list_annotate (add_fsfun_supp_all f1 f2)
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A
Ha: f1 a + f2 a ≠ 0

dexist a Ha ∈ list_annotate (add_fsfun_supp_all f1 f2)
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A
Ha: f1 a + f2 a ≠ 0

`(dexist a Ha) ∈ elements (list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2))
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A
Ha: f1 a + f2 a ≠ 0

f1 a ≠ 0 ∨ f2 a ≠ 0
by lia. Qed.
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

add_fsfun f1 f2 a = f1 a + f2 a
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

add_fsfun f1 f2 a = f1 a + f2 a
done. Qed.
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> equiv ==> equiv) add_fsfun
A: Type
EqDecision0: EqDecision A

Proper (equiv ==> equiv ==> equiv) add_fsfun
A: Type
EqDecision0: EqDecision A
f1, g1: fsfun A 0
Heqv1: f1 ≡ g1
f2, g2: fsfun A 0
Heqv2: f2 ≡ g2

add_fsfun f1 f2 ≡ add_fsfun g1 g2
A: Type
EqDecision0: EqDecision A
f1, g1: fsfun A 0
Heqv1: f1 ≡ g1
f2, g2: fsfun A 0
Heqv2: f2 ≡ g2
a: A

add_fsfun f1 f2 a = add_fsfun g1 g2 a
by rewrite !add_fsfun_rew, Heqv1, Heqv2. Qed.
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, a ∈ fin_supp (add_fsfun f1 f2) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, a ∈ fin_supp (add_fsfun f1 f2) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

a ∈ map proj1_sig (list_annotate (add_fsfun_supp_all f1 f2)) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

a ∈ add_fsfun_supp f1 f2 ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

a ∈ list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2
by rewrite elem_of_union, !elem_of_list_to_set. Qed.
A: Type
EqDecision0: EqDecision A

Comm equiv add_fsfun
A: Type
EqDecision0: EqDecision A

Comm equiv add_fsfun
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A

add_fsfun f1 f2 a = add_fsfun f2 f1 a
by rewrite !add_fsfun_rew; lia. Qed.
A: Type
EqDecision0: EqDecision A

LeftId equiv zero_fsfun add_fsfun
A: Type
EqDecision0: EqDecision A

LeftId equiv zero_fsfun add_fsfun
by intro; apply fsfun_equiv_unfold; extensionality a. Qed.
A: Type
EqDecision0: EqDecision A

RightId equiv zero_fsfun add_fsfun
A: Type
EqDecision0: EqDecision A

RightId equiv zero_fsfun add_fsfun
A: Type
EqDecision0: EqDecision A
x: fsfun A 0
a: A

add_fsfun x zero_fsfun a = x a
by rewrite add_fsfun_rew, zero_fsfun_rew; lia. Qed.
A: Type
EqDecision0: EqDecision A

Assoc equiv add_fsfun
A: Type
EqDecision0: EqDecision A

Assoc equiv add_fsfun
A: Type
EqDecision0: EqDecision A
f, g, h: fsfun A 0
a: A

add_fsfun f (add_fsfun g h) a = add_fsfun (add_fsfun f g) h a
by rewrite !add_fsfun_rew; lia. Qed.
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, add_fsfun (succ_fsfun f1 a) f2 ≡ succ_fsfun (add_fsfun f1 f2) a
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, add_fsfun (succ_fsfun f1 a) f2 ≡ succ_fsfun (add_fsfun f1 f2) a
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a, a': A

add_fsfun (succ_fsfun f1 a) f2 a' = succ_fsfun (add_fsfun f1 f2) a a'
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a, a': A

succ_fsfun f1 a a' + f2 a' = succ_fsfun (add_fsfun f1 f2) a a'
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a': A

succ_fsfun f1 a' a' + f2 a' = succ_fsfun (add_fsfun f1 f2) a' a'
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a, a': A
n: a ≠ a'
succ_fsfun f1 a a' + f2 a' = succ_fsfun (add_fsfun f1 f2) a a'
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a': A

succ_fsfun f1 a' a' + f2 a' = succ_fsfun (add_fsfun f1 f2) a' a'
by rewrite !succ_fsfun_eq.
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a, a': A
n: a ≠ a'

succ_fsfun f1 a a' + f2 a' = succ_fsfun (add_fsfun f1 f2) a a'
by rewrite !succ_fsfun_neq. Qed.
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, add_fsfun f2 (succ_fsfun f1 a) ≡ succ_fsfun (add_fsfun f2 f1) a
A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0

a : A, add_fsfun f2 (succ_fsfun f1 a) ≡ succ_fsfun (add_fsfun f2 f1) a
by intros; rewrite (comm add_fsfun), add_fsfun_succ_l, (comm add_fsfun). Qed.
To be able to prove things by induction on finitely supported functions on naturals we define the following inductive property and then we show that it holds for all such functions.
Inductive NatFSFun : fsfun A 0 -> Prop :=
| P_zero :
    forall (f' : fsfun A 0), f' ≡ zero_fsfun ->
    NatFSFun f'
| P_succ :
    forall (f : fsfun A 0), NatFSFun f ->
    forall (f' : fsfun A 0) (i : A), f' ≡ succ_fsfun f i ->
    NatFSFun f'.

A: Type
EqDecision0: EqDecision A
f: fsfun A 0

NatFSFun f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0

NatFSFun f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: nat
Heqn: n = fsfun_sum f

NatFSFun f
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: nat
Heqn: fsfun_sum f = n

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n

Exists (λ i : A, f i ≠ 0) (fin_supp f)
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n

Exists (λ i : A, f i ≠ 0) (fin_supp f)
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: ¬ Exists (λ i : A, f i ≠ 0) (fin_supp f)

False
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)

False
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)

0 = fsfun_sum f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)

fsfun_sum f = 0
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)

i : A, i ∈ fin_supp f → f i = 0
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)
a: A
Ha: a ∈ fin_supp f

f a = 0
by rewrite Forall_forall in Hex; apply Hex in Ha; cbn in Ha; lia.
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
Hx: f (Exists_choose_first Hex) ≠ 0

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
Hx: f (Exists_choose_first Hex) ≠ 0
x:= Exists_choose_first Hex: A

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0

f ≡ succ_fsfun f' x
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0
Heq: f ≡ succ_fsfun f' x
NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0

f ≡ succ_fsfun f' x
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
a: A

f a = succ_fsfun (update_fsfun f x px) x a
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
px: nat
a: A
Heqx: f a = S px

f a = succ_fsfun (update_fsfun f a px) a a
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
a: A
n0: x ≠ a
f a = succ_fsfun (update_fsfun f x px) x a
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
px: nat
a: A
Heqx: f a = S px

f a = succ_fsfun (update_fsfun f a px) a a
by rewrite succ_fsfun_eq, update_fsfun_eq.
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
a: A
n0: x ≠ a

f a = succ_fsfun (update_fsfun f x px) x a
by rewrite succ_fsfun_neq, update_fsfun_neq.
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0
Heq: f ≡ succ_fsfun f' x

NatFSFun f
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
f':= update_fsfun f x px: fsfun A 0
Heq: f ≡ succ_fsfun f' x

NatFSFun f'
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Heqn: fsfun_sum f = S n
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
Heq: f ≡ succ_fsfun (update_fsfun f x px) x

fsfun_sum (update_fsfun f x px) = n
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
Heq: f ≡ succ_fsfun (update_fsfun f x px) x
Heqn: fsfun_sum (succ_fsfun (update_fsfun f x px) x) = S n

fsfun_sum (update_fsfun f x px) = n
A: Type
EqDecision0: EqDecision A
n: nat
IHn: f : fsfun A 0, fsfun_sum f = n → NatFSFun f
f: fsfun A 0
Hex: Exists (λ i : A, f i ≠ 0) (fin_supp f)
x:= Exists_choose_first Hex: A
px: nat
Heqx: f x = S px
Heq: f ≡ succ_fsfun (update_fsfun f x px) x
Heqn: S (fsfun_sum (update_fsfun f x px)) = S n

fsfun_sum (update_fsfun f x px) = n
by congruence. Qed.
A: Type
EqDecision0: EqDecision A
f: fsfun A 0

f ≡ zero_fsfun ∨ ( (a : A) (f' : fsfun A 0), f ≡ succ_fsfun f' a)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0

f ≡ zero_fsfun ∨ ( (a : A) (f' : fsfun A 0), f ≡ succ_fsfun f' a)
A: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hcomplete: NatFSFun f

f ≡ zero_fsfun ∨ ( (a : A) (f' : fsfun A 0), f ≡ succ_fsfun f' a)
by inversion Hcomplete; subst; [left | right; eexists _,_]. Qed.
A: Type
EqDecision0: EqDecision A
P: fsfun A 0Prop
Hproper: Proper (equiv ==> impl) P
Hzero: P zero_fsfun
Hsucc: (i : A) (f : fsfun A 0), P f → P (succ_fsfun f i)

f : fsfun A 0, P f
A: Type
EqDecision0: EqDecision A
P: fsfun A 0Prop
Hproper: Proper (equiv ==> impl) P
Hzero: P zero_fsfun
Hsucc: (i : A) (f : fsfun A 0), P f → P (succ_fsfun f i)

f : fsfun A 0, P f
A: Type
EqDecision0: EqDecision A
P: fsfun A 0Prop
Hproper: Proper (equiv ==> impl) P
Hzero: P zero_fsfun
Hsucc: (i : A) (f : fsfun A 0), P f → P (succ_fsfun f i)
f: fsfun A 0

P f
A: Type
EqDecision0: EqDecision A
P: fsfun A 0Prop
Hproper: Proper (equiv ==> impl) P
Hzero: P zero_fsfun
Hsucc: (i : A) (f : fsfun A 0), P f → P (succ_fsfun f i)
f: fsfun A 0
Hcomplete: NatFSFun f

P f
by induction Hcomplete as [| ? ? ? ? ? ->]; [eapply Hproper | apply Hsucc]. Qed. End sec_fsfun_fixed_domain.