Progress table.v #29
Progress table.v #29
Conversation
| move=> t /andP []; case: (ltngtP i (size s)) => [lt_is|lt_si|->]. | ||
| - rewrite -lindex_gt -?rindex_le //= ?ltnS ?size_map ?(ltnW lt_is) //. | ||
| move=> + ge_i; apply: contra_leqF => ts; move: ge_i. | ||
| by rewrite lindex_in ?rindex_in ?sorted_map ?mem_map ?map_inj_uniq. | ||
| - by rewrite nth_default //= size_map. | ||
| - move=> + _; apply: contra_ltF => ts. | ||
| rewrite -lindex_le //= ?ltnS ?size_map //. | ||
| by rewrite -(size_map Fin) -has_find has_map; apply/hasP; exists t => /=. |
There was a problem hiding this comment.
I have an unpushed commit, does this work?
| move=> t /andP []; case: (ltngtP i (size s)) => [lt_is|lt_si|->]. | |
| - rewrite -lindex_gt -?rindex_le //= ?ltnS ?size_map ?(ltnW lt_is) //. | |
| move=> + ge_i; apply: contra_leqF => ts; move: ge_i. | |
| by rewrite lindex_in ?rindex_in ?sorted_map ?mem_map ?map_inj_uniq. | |
| - by rewrite nth_default //= size_map. | |
| - move=> + _; apply: contra_ltF => ts. | |
| rewrite -lindex_le //= ?ltnS ?size_map //. | |
| by rewrite -(size_map Fin) -has_find has_map; apply/hasP; exists t => /=. | |
| rewrite -(@lindexE i t); last by rewrite inE t_gt ltW. | |
| by apply: contraTF => /mem_rnext->; rewrite ltxx. |
There was a problem hiding this comment.
@CohenCyril There is no lemma lindexE. Do you mean lindex_eq?
There was a problem hiding this comment.
mem_rnext is also missing.
There was a problem hiding this comment.
I need to check what I had, I think I have 5 different variations son my hard drive, and I need to decide which one of them is actually useful...
There was a problem hiding this comment.
I think I waited for the new interval.v to start anew
There was a problem hiding this comment.
because in the current state, I need a few variations snext, anext and stuff, whereas providing an interval bound would explain whether or not we want to include the starting point or not in the search!
There was a problem hiding this comment.
There would be a unique next b function such that if b is BLeft x it includes x and otherwise not...
I'm quite excited about that and I wished to continue exploring this direction.
There was a problem hiding this comment.
(as soon as mathcomp 1.12 got merged)
There was a problem hiding this comment.
because in the current state, I need a few variations
snext,anextand stuff, ...
Sure. I see this is confusing and frustrating😂
|
|
||
| Lemma lrindex_notin i : | ||
| {in [pred t | [i] < t%:x < [i.+1]], forall t, t \notin s}. | ||
| Proof. (* by move=> x /lindex_inF->. Qed. *) Admitted. | ||
| Proof. by move=> x /ext_inF ->. Qed. | ||
|
|
||
| Lemma lindex_next t tnext : anext t = tnext%:x -> lindex s tnext = lindex s t. | ||
| (* Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed. *) |
There was a problem hiding this comment.
| (* Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed. *) | |
| Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed. |
| Lemma in_aprev t : aprev t \in -oo :: map Fin s. | ||
| Proof. | ||
| by rewrite aprevE; case: ifPn => [ts|_]; rewrite ?in_sprev// in_cons mem_map. | ||
| Qed. | ||
| Proof. by apply: mem_nth; rewrite /= ltnS size_map rindex_size. Qed. |
There was a problem hiding this comment.
Remark: in_aprev and in_anext (below) do not require s to be sorted, but they accidentally required this assumption (by using aprevE?) in the previous version. We should reshuffle sections or declare Argument commands to avoid this kind of issue.
lindexandrindexare relocated since I had to use some of them for sequences of extended values.ext_inFandlrindex_notin.