diff options
| author | Georges Gonthier | 2019-11-22 10:02:04 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2019-11-22 10:02:04 +0100 |
| commit | 317267c618ecff861ec6539a2d6063cef298d720 (patch) | |
| tree | 8b9f3af02879faf1bba3ee9e7befcb52f44107ed /mathcomp/ssreflect/binomial.v | |
| parent | b1ca6a9be6861f6c369db642bc194cf78795a66f (diff) | |
New generalised induction idiom (#434)
Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
either new helper lemmas `ubnP` and `ltnSE` or a specific `nat`
induction principle `ltn_ind`.
Added (non-strict in)equality induction helper lemmas
Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression
along with some (in)equality, in preparation for some generalised
induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed
`ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember
that the inductive value remains below the initial one.
Used the change log to give notice to users to update the generalised
induction idioms in their proofs to one of the new forms before
Mathcomp 1.11.
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 0c5be52..8bdb426 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -508,13 +508,13 @@ suffices [le_i_ti le_ti_ni]: i <= tnth t i /\ tnth t i <= i + n. by rewrite /sub_mn inordK ?subnKC // ltnS leq_subLR. pose y0 := tnth t i; rewrite (tnth_nth y0) -(nth_map _ (val i)) ?size_tuple //. case def_e: (map _ _) => [|x e] /=; first by rewrite nth_nil ?leq_addr. -rewrite def_e in inc_t; split. - case: {-2}i; rewrite /= -{1}(size_tuple t) -(size_map val) def_e. - elim=> //= j IHj lt_j_t; apply: leq_trans (pathP (val i) inc_t _ lt_j_t). - by rewrite ltnS IHj 1?ltnW. +set nth_i := nth (i : nat); rewrite def_e in inc_t; split. + have: i < size (x :: e) by rewrite -def_e size_map size_tuple ltn_ord. + elim: (val i) => //= j IHj lt_j_e. + by apply: leq_trans (pathP (val i) inc_t _ lt_j_e); rewrite ltnS IHj 1?ltnW. move: (_ - _) (subnK (valP i)) => k /=. -elim: k {-2}(val i) => /= [|k IHk] j def_m; rewrite -ltnS -addSn. - by rewrite [j.+1]def_m -def_e (nth_map y0) ?ltn_ord // size_tuple -def_m. +elim: k (val i) => /= [|k IHk] j; rewrite -ltnS -addSn ?add0n => def_m. + by rewrite def_m -def_e /nth_i (nth_map y0) ?ltn_ord // size_tuple -def_m. rewrite (leq_trans _ (IHk _ _)) -1?addSnnS //; apply: (pathP _ inc_t). rewrite -ltnS (leq_trans (leq_addl k _)) // -addSnnS def_m. by rewrite -(size_tuple t) -(size_map val) def_e. |