Pset3: theorems bst_strict_monotone_increasing and bst_strict_monotone_decreasing_mirror are degenerate #1

Activity

1. malcolmsharpe commented on Aug 24, 2022

   

   malcolmsharpe

   on Aug 24, 2022

   Author

   More actions

   Update with a proposed fix:

   On further thought, there are actually two underlying issues.

   1. It's too strong to require that f be onto. That rules out perfectly reasonable functions such as f(x) = x^2, which is strictly increasing on the natural numbers. This is a problem for both theorem statements.
   2. There are no strictly decreasing functions from nat to nat. This is a problem for the second theorem statement only.

   For issue 1, the root cause is the way Q is specified. All we actually need is, if P = {x_1,...,x_n}, then Q = {f(x_1),...,f(x_n)}. The current conditions are too strong. We can fix by defining Q as follows: Q := fun a => exists x, a = f x /\ P x.

   For issue 2, either a non-nat set is needed (e.g. general integers would be fine), or the monotonicity condition must be weakened. The second fix is self-contained to the theorem statement, so that's what I use below.

   Here are my proposed fixed theorem statements:

     Theorem bst_strict_monotone_increasing_fixed : forall tr P f,
         bst tr P ->
         (forall x y, x < y <-> f x < f y) ->
         bst (tree_map f tr) (fun a => exists x, a = f x /\ P x).
   

     Theorem bst_strict_monotone_decreasing_mirror_fixed : forall tr P f,
         bst tr P ->
         (forall x y, P x -> P y -> x < y <-> f x > f y) ->
         bst (mirror (tree_map f tr)) (fun a => exists x, a = f x /\ P x).