From Coq Require Import FunctionalExtensionality. From stdpp Require Import prelude finite. From VLSM.Lib Require Import Preamble StdppExtras ListExtras FinSetExtras.
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: BEquivalence equivA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BEquivalence equivA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BEquivalence (λ f g : fsfun A b, f = g)A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BSymmetric (λ f g : fsfun A b, f = g)A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BTransitive (λ f g : fsfun A b, f = g)by intros f g; apply symmetry.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BSymmetric (λ 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: BTransitive (λ f g : fsfun A b, f = g)A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq) fsfun_projectby intros f g Heqv; inversion Heqv. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq) fsfun_projectA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq) projT1by apply fsfun_project_proper. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq) projT1A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A bf ≡ g ↔ f = gdone. 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, g: fsfun A bf ≡ g ↔ f = gA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b∀ a : A, a ∈ fin_supp f ↔ f a ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b∀ a : A, a ∈ fin_supp f ↔ f a ≠ bA: 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 ≠ bA: 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 ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: Af 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 ≠ bby 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
asupp: {x : A | bool_decide (f x ≠ b)}f (`asupp) ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: Af 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
Ha: 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, a ∉ fin_supp f ↔ f a = bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b∀ a : A, a ∉ fin_supp f ↔ f a = bby destruct (decide (f a = b)); itauto. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
a: A¬ f a ≠ b ↔ f a = bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A bNoDup (fin_supp f)by apply dsig_NoDup_map, NoDup_enum. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A bNoDup (fin_supp f)A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> Permutation) fin_suppA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> Permutation) fin_suppA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heq: f ≡ gfin_supp f ≡ₚ fin_supp gby intro; rewrite !elem_of_fin_supp, Heq. Qed.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 gA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BRelDecision equivA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BRelDecision equivA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A bDecision (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)by rewrite Heqv in Hneqv.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 ≡ gFalseA: 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: Af a = g aA: 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 ff a = g aA: 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 gf a = g aby 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
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 = bf a = g aA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BNoDup []by constructor. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BNoDup []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∀ x : support b (const b), x ∈ []A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: Bfin_supp empty_fsfun = []done. Qed.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: Bfin_supp empty_fsfun = []A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A bfin_supp f = [] → f ≡ empty_fsfunA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A bfin_supp f = [] → f ≡ empty_fsfunA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
Hf: fin_supp f = []
a: Af a = empty_fsfun aA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
Hf: fin_supp f = []
a: Aa ∉ fin_supp fby 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
Hf: fin_supp f = []
a: Aa ∉ []A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': BForall (λ 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': BForall (λ 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': BForall (λ 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: Aa ∈ 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 ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: Aa ∈ (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 ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = ba ∈ list_to_set (fin_supp f) ∖ {[n]} → update f n b' a ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ ba ∈ {[n]} ∪ list_to_set (fin_supp f) → update f n b' a ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' = ba ∈ list_to_set (fin_supp f) ∖ {[n]} → update f n b' a ≠ bby 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' = bf a ≠ b ∧ a ≠ n → update f n b' a ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ ba ∈ {[n]} ∪ list_to_set (fin_supp f) → update f n b' a ≠ bby 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
a: A
H: b' ≠ ba = n ∨ f a ≠ b → update f n b' a ≠ bA: 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), 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) (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 ≠ bdexist 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]}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' = bf a ≠ b ∧ a ≠ nA: 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)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
a: A
Ha: update f n b' a ≠ b
H: b' ≠ ba = n ∨ f a ≠ bA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': Bupdate_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': Bupdate_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∀ m : A, m ≠ n → update_fsfun f n b' m = f mby intros; setoid_rewrite update_neq. 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 mA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq ==> eq ==> equiv) update_fsfunA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: BProper (equiv ==> eq ==> eq ==> equiv) update_fsfunA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
n: A
b': Bupdate_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: Aupdate_fsfun f n b' a = update_fsfun g n b' aA: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
b': B
a: Aupdate_fsfun f a b' a = update_fsfun g a b' aA: 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 ≠ aupdate_fsfun f n b' a = update_fsfun g n b' aby rewrite !update_fsfun_eq.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f, g: fsfun A b
Heqv: f ≡ g
b': B
a: Aupdate_fsfun f a b' a = update_fsfun g a b' aby rewrite !update_fsfun_neq, Heqv. Qed.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 ≠ aupdate_fsfun f n b' a = update_fsfun g n b' aA: 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: Aa ∈ 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: Aa ∈ 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' = ba ∈ 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' ≠ ba ∈ {[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_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' = ba ∈ 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_union, elem_of_list_to_set, elem_of_singleton; split; itauto. Qed. End sec_fsfun_fixed_supp_value.A: Type
EqDecision0: EqDecision A
B: Type
EqDecision1: EqDecision B
b: B
f: fsfun A b
n: A
b': B
a: A
H: b' ≠ ba ∈ {[n]} ∪ list_to_set (fin_supp f) ↔ b' = b ∧ a ∈ fin_supp f ∧ a ≠ n ∨ b' ≠ b ∧ (a ∈ fin_supp f ∨ a = n)
Definition zero_fsfun : fsfun A 0 := empty_fsfun.A: Type
EqDecision0: EqDecision A∀ n : A, zero_fsfun n = 0done. 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∀ n : A, zero_fsfun n = 0A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: Asucc_fsfun f n n = S (f n)by apply update_fsfun_eq. Qed.A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: Asucc_fsfun f n n = S (f n)A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A∀ m : A, m ≠ n → succ_fsfun f n m = f mby apply update_fsfun_neq. Qed.A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A∀ m : A, m ≠ n → succ_fsfun f n m = f mA: Type
EqDecision0: EqDecision AProper (equiv ==> eq ==> equiv) succ_fsfunA: Type
EqDecision0: EqDecision AProper (equiv ==> eq ==> equiv) succ_fsfunby apply update_fsfun_proper; [.. | rewrite Heqv]. Qed.A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ g
n: Asucc_fsfun f n ≡ succ_fsfun g nA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A∀ a : A, a ∈ fin_supp (succ_fsfun f n) ↔ a = n ∨ a ∈ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A∀ a : A, a ∈ fin_supp (succ_fsfun f n) ↔ a = n ∨ a ∈ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: Aa ∈ fin_supp (update_fsfun f n (S (f n))) ↔ a = n ∨ a ∈ fin_supp fby split; itauto lia. Qed.A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n, a: AS (f n) = 0 ∧ a ∈ fin_supp f ∧ a ≠ n ∨ S (f n) ≠ 0 ∧ (a ∈ fin_supp f ∨ a = n) ↔ a = n ∨ a ∈ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: An ∈ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: An ∈ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp ffin_supp (succ_fsfun f n) ≡ₚ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp f
x: Ax ∈ fin_supp (succ_fsfun f n) ↔ x ∈ fin_supp fby set_solver. Qed.A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∈ fin_supp f
x: Ax = n ∨ x ∈ fin_supp f ↔ x ∈ fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: An ∉ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ n :: fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: An ∉ fin_supp f → fin_supp (succ_fsfun f n) ≡ₚ n :: fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∉ fin_supp felements (update_supp f n (S (f n))) ≡ₚ n :: fin_supp fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: A
H: n ∉ fin_supp felements ({[n]} ∪ list_to_set (fin_supp f)) ≡ₚ n :: fin_supp fby 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
f: fsfun A 0
n: A
H: n ∉ fin_supp fn :: elements (list_to_set (fin_supp f)) ≡ₚ n :: fin_supp fA: Type
EqDecision0: EqDecision A
n: Adelta_nat_fsfun n n = 1by apply succ_fsfun_eq. Qed.A: Type
EqDecision0: EqDecision A
n: Adelta_nat_fsfun n n = 1A: Type
EqDecision0: EqDecision A
n: A∀ m : A, m ≠ n → delta_nat_fsfun n m = 0by apply succ_fsfun_neq. Qed.A: Type
EqDecision0: EqDecision A
n: A∀ m : A, m ≠ n → delta_nat_fsfun n m = 0A: Type
EqDecision0: EqDecision A
n: A∀ a : A, a ∈ fin_supp (delta_nat_fsfun n) ↔ a = nA: Type
EqDecision0: EqDecision A
n: A∀ a : A, a ∈ fin_supp (delta_nat_fsfun n) ↔ a = nA: Type
EqDecision0: EqDecision A
n, a: Aa ∈ fin_supp (delta_nat_fsfun n) ↔ a = nA: Type
EqDecision0: EqDecision A
n, a: Aa ∈ fin_supp (succ_fsfun zero_fsfun n) ↔ a = nby itauto. Qed. Definition fsfun_sum (f : fsfun A 0) : nat := sum_list_with f (fin_supp f).A: Type
EqDecision0: EqDecision A
n, a: Aa = n ∨ False ↔ a = nA: Type
EqDecision0: EqDecision AProper (equiv ==> eq) fsfun_sumA: Type
EqDecision0: EqDecision AProper (equiv ==> eq) fsfun_sumA: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ gfsfun_sum f = fsfun_sum gA: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ gsum_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 ≡ gsum_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 ≡ gfin_supp f ≡ₚ fin_supp gby apply sum_list_with_ext_forall; intros; rewrite Heqv.A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ gsum_list_with f (fin_supp g) = sum_list_with g (fin_supp g)by apply fin_supp_proper. Qed.A: Type
EqDecision0: EqDecision A
f, g: fsfun A 0
Heqv: f ≡ gfin_supp f ≡ₚ fin_supp gA: Type
EqDecision0: EqDecision A
f: fsfun A 0fsfun_sum f = 0 → f ≡ zero_fsfunA: Type
EqDecision0: EqDecision A
f: fsfun A 0fsfun_sum f = 0 → f ≡ zero_fsfunA: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: ∀ i : A, i ∈ fin_supp f → f i = 0f ≡ zero_fsfunA: Type
EqDecision0: EqDecision A
f: fsfun A 0
Hall: ∀ i : A, i ∈ fin_supp f → f i = 0
a: Af a = zero_fsfun aA: 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 aFalseby apply Hall in Ha'. Qed.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 fFalseA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: Afsfun_sum (succ_fsfun f n) = S (fsfun_sum f)A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: Afsfun_sum (succ_fsfun f n) = S (fsfun_sum f)A: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: Asum_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 fsum_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 fsum_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 fsum_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 fsum_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: ANoDup (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 lsucc_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 ∈ lsucc_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 lsucc_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 lS (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 lsum_list_with (succ_fsfun f n) l = sum_list_with f lby intros; rewrite succ_fsfun_neq by set_solver.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 iA: 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 ∈ lsucc_fsfun f n 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: 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 ∈ lf 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
n0: n ∉ fin_supp fsum_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 fsum_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 fS (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 f1 + 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 fsum_list_with (succ_fsfun f n) (fin_supp f) = sum_list_with f (fin_supp f)by intros; rewrite succ_fsfun_neq; [| set_solver]. Qed.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
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 0Forall (λ a : A, f1 a + f2 a ≠ 0) (elements (add_fsfun_supp f1 f2))A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0Forall (λ a : A, f1 a + f2 a ≠ 0) (elements (add_fsfun_supp f1 f2))A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aa ∈ elements (list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2)) → f1 a + f2 a ≠ 0by 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
a: Af1 a ≠ 0 ∨ f2 a ≠ 0 → f1 a + f2 a ≠ 0A: 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, NoDup (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) (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 ≠ 0dexist 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))by lia. Qed.A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: A
Ha: f1 a + f2 a ≠ 0f1 a ≠ 0 ∨ f2 a ≠ 0A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aadd_fsfun f1 f2 a = f1 a + f2 adone. Qed.A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aadd_fsfun f1 f2 a = f1 a + f2 aA: Type
EqDecision0: EqDecision AProper (equiv ==> equiv ==> equiv) add_fsfunA: Type
EqDecision0: EqDecision AProper (equiv ==> equiv ==> equiv) add_fsfunA: Type
EqDecision0: EqDecision A
f1, g1: fsfun A 0
Heqv1: f1 ≡ g1
f2, g2: fsfun A 0
Heqv2: f2 ≡ g2add_fsfun f1 f2 ≡ add_fsfun g1 g2by rewrite !add_fsfun_rew, Heqv1, Heqv2. Qed.A: Type
EqDecision0: EqDecision A
f1, g1: fsfun A 0
Heqv1: f1 ≡ g1
f2, g2: fsfun A 0
Heqv2: f2 ≡ g2
a: Aadd_fsfun f1 f2 a = add_fsfun g1 g2 aA: 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 f2A: 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 f2A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aa ∈ map proj1_sig (list_annotate (add_fsfun_supp_all f1 f2)) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aa ∈ add_fsfun_supp f1 f2 ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2by rewrite elem_of_union, !elem_of_list_to_set. Qed.A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aa ∈ list_to_set (fin_supp f1) ∪ list_to_set (fin_supp f2) ↔ a ∈ fin_supp f1 ∨ a ∈ fin_supp f2A: Type
EqDecision0: EqDecision AComm equiv add_fsfunA: Type
EqDecision0: EqDecision AComm equiv add_fsfunby rewrite !add_fsfun_rew; lia. Qed.A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a: Aadd_fsfun f1 f2 a = add_fsfun f2 f1 aA: Type
EqDecision0: EqDecision ALeftId equiv zero_fsfun add_fsfunby intro; apply fsfun_equiv_unfold; extensionality a. Qed.A: Type
EqDecision0: EqDecision ALeftId equiv zero_fsfun add_fsfunA: Type
EqDecision0: EqDecision ARightId equiv zero_fsfun add_fsfunA: Type
EqDecision0: EqDecision ARightId equiv zero_fsfun add_fsfunby rewrite add_fsfun_rew, zero_fsfun_rew; lia. Qed.A: Type
EqDecision0: EqDecision A
x: fsfun A 0
a: Aadd_fsfun x zero_fsfun a = x aA: Type
EqDecision0: EqDecision AAssoc equiv add_fsfunA: Type
EqDecision0: EqDecision AAssoc equiv add_fsfunby rewrite !add_fsfun_rew; lia. Qed.A: Type
EqDecision0: EqDecision A
f, g, h: fsfun A 0
a: Aadd_fsfun f (add_fsfun g h) a = add_fsfun (add_fsfun f g) h aA: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0∀ a : A, add_fsfun (succ_fsfun f1 a) f2 ≡ succ_fsfun (add_fsfun f1 f2) aA: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0∀ a : A, add_fsfun (succ_fsfun f1 a) f2 ≡ succ_fsfun (add_fsfun f1 f2) aA: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a, a': Aadd_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': Asucc_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': Asucc_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'by rewrite !succ_fsfun_eq.A: Type
EqDecision0: EqDecision A
f1, f2: fsfun A 0
a': Asucc_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': 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, add_fsfun f2 (succ_fsfun f1 a) ≡ succ_fsfun (add_fsfun f2 f1) aby intros; rewrite (comm add_fsfun), add_fsfun_succ_l, (comm add_fsfun). 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
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 0NatFSFun fA: Type
EqDecision0: EqDecision A
f: fsfun A 0NatFSFun fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: nat
Heqn: n = fsfun_sum fNatFSFun fA: Type
EqDecision0: EqDecision A
f: fsfun A 0
n: nat
Heqn: fsfun_sum f = nNatFSFun fA: 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 nNatFSFun fA: 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 nExists (λ 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 fA: 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 nExists (λ 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)FalseA: 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)FalseA: 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 fA: 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 = 0A: 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 = 0by 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: Forall (not ∘ (λ i : A, f i ≠ 0)) (fin_supp f)
a: A
Ha: a ∈ fin_supp ff a = 0A: 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 fA: 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) ≠ 0NatFSFun fA: 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: ANatFSFun fA: 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 pxNatFSFun fA: 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 0NatFSFun fA: 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 0f ≡ succ_fsfun f' xA: 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' xNatFSFun fA: 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 0f ≡ succ_fsfun f' xA: 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: Af a = succ_fsfun (update_fsfun f x px) x aA: 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 pxf a = succ_fsfun (update_fsfun f a px) a aA: 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 ≠ af a = succ_fsfun (update_fsfun f x px) x aby 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)
px: nat
a: A
Heqx: f a = S pxf a = succ_fsfun (update_fsfun f a px) a aby 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
a: A
n0: x ≠ af a = succ_fsfun (update_fsfun f x px) x aA: 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' xNatFSFun fA: 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' xNatFSFun 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) xfsfun_sum (update_fsfun f x px) = nA: 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 nfsfun_sum (update_fsfun f x px) = nby congruence. Qed.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 nfsfun_sum (update_fsfun f x px) = nA: Type
EqDecision0: EqDecision A
f: fsfun A 0f ≡ zero_fsfun ∨ (∃ (a : A) (f' : fsfun A 0), f ≡ succ_fsfun f' a)A: Type
EqDecision0: EqDecision A
f: fsfun A 0f ≡ 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
f: fsfun A 0
Hcomplete: NatFSFun ff ≡ zero_fsfun ∨ (∃ (a : A) (f' : fsfun A 0), f ≡ succ_fsfun f' a)A: Type
EqDecision0: EqDecision A
P: fsfun A 0 → Prop
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 fA: Type
EqDecision0: EqDecision A
P: fsfun A 0 → Prop
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 fA: Type
EqDecision0: EqDecision A
P: fsfun A 0 → Prop
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 0P fby induction Hcomplete as [| ? ? ? ? ? ->]; [eapply Hproper | apply Hsucc]. Qed. End sec_fsfun_fixed_domain.A: Type
EqDecision0: EqDecision A
P: fsfun A 0 → Prop
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 fP f