diff options
| author | Erik Martin-Dorel | 2019-02-27 17:31:35 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-03-20 12:54:26 +0100 |
| commit | c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (patch) | |
| tree | 73c109057bf3f18127be887fcc1b2e0ba82ff3e2 /mathcomp/ssreflect/finfun.v | |
| parent | 4c8455594c5adff08761037a5919c058d0d502ba (diff) | |
Add extra eta lemmas for the under tactic
Related: coq/coq#9651
Diffstat (limited to 'mathcomp/ssreflect/finfun.v')
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index db1a8e7..01576fe 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -128,6 +128,10 @@ split=> [eq_f12 | -> //]; do 2!apply: val_inj => /=. by rewrite !fgraph_codom /= (eq_codom eq_f12). Qed. +Lemma eq_ffun (g1 g2 : aT -> rT) : + g1 =1 g2 -> finfun g1 = finfun g2. +Proof. by move=> eq_g; apply/ffunP => x; rewrite !ffunE eq_g. Qed. + Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT). Proof. by move=> f; apply/ffunP/ffunE. Qed. @@ -148,6 +152,7 @@ Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). Arguments ffunK {aT rT}. +Arguments eq_ffun {aT rT} [g1] g2 eq_g12. Arguments familyP {aT rT pT F f}. Arguments ffun_onP {aT rT R f}. |