Merge pull request #292 from erikmd/under-support

Add extra eta lemmas for the under tactic

3 files changed, 14 insertions, 2 deletions

diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index d3487f5..f8b732a 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -132,6 +132,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.
 
@@ -152,6 +156,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}.
 
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 8e174c0..72bfe74 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -239,11 +239,15 @@ Proof. by rewrite in_set. Qed.
 Lemma eqsVneq A B : {A = B} + {A != B}.
 Proof. exact: eqVneq. Qed.
 
+Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB.
+Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed.
+
 End BasicSetTheory.
 
 Definition inE := (in_set, inE).
 
 Arguments set0 {T}.
+Arguments eq_finset {T} [pA] pB eq_pAB.
 Hint Resolve in_setT : core.
 
 Notation "[ 'set' : T ]" := (setTfor (Phant T))
@@ -2211,4 +2215,3 @@ Arguments setCK {T}.
 Arguments minsetP {T P A}.
 Arguments maxsetP {T P A}.
 Prenex Implicits minset maxset.
-
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 8f81155..c0ba403 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -411,10 +411,14 @@ Proof. by rewrite -tnth_nth tnth_mktuple. Qed.
 
 End MkTuple.
 
+Lemma eq_mktuple T' (f1 f2 : 'I_n -> T') :
+  f1 =1 f2 -> mktuple f1 = mktuple f2.
+Proof. by move=> eq_f; apply eq_from_tnth=> i; rewrite !tnth_map eq_f. Qed.
+
 End UseFinTuple.
 
 Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n => F))
   (at level 0, i at level 0,
    format "[ '[hv' 'tuple'  F '/'   |  i  <  n ] ']'") : form_scope.
 
-
+Arguments eq_mktuple {n T'} [f1] f2 eq_f12.