proposition: Lemma wf_R : well_founded R.
proof: Proof. pose F := (fun (f : nat -> option nat) => list_sum (map (fun p => if f p is None then 1 else 0) (seq 0 l))). pose G := (fun (f : nat -> option nat) => list_sum (map (fun p => if f p is Some c then c else 0) (seq 0 l))). elim /(Nat.measure_induction _ F). elim /(Nat.measure_induction _ G). move=> f IHG IHF. constructor => g Hgf. case: Hgf IHG IHF. - move=> {}f p c ? Hf IHG IHF. apply: IHF. rewrite /F. have /list_sum_map_lt : In p (seq 0 l) by (apply /in_seq; lia). apply. + move=> p''. case Hp'': (f p'') => [c''|]. * rewrite /update Hp''. by case: (Nat.eq_dec p'' p). * rewrite /update Hp''. case: (Nat.eq_dec p'' p); lia. + rewrite /update Hf. case: (Nat.eq_dec p p); lia. - move=> c' {}f p c Hl Hf ? IHG IHF. apply: IHG; first last. { move=> h Hh. apply: IHF. suff: F (update f p (Some c)) <= F f by lia. apply: list_sum_map_le. move=> p''. case Hp'': (f p'') => [c''|]. - rewrite /update Hp''. by case: (Nat.eq_dec p'' p). - rewrite /update Hp''. case: (Nat.eq_dec p'' p); lia. } rewrite /G. have : In p (seq 0 l) by (apply /in_seq; lia). move=> /list_sum_map_lt. apply. + move=> p''. case Hp'': (f p'') => [c''|]. * rewrite /update. case: (Nat.eq_dec p'' p). ** move=> ?. subst. move: Hf Hp'' => -> []. lia. ** rewrite Hp''. lia. * rewrite /update. case: (Nat.eq_dec p'' p). ** move=> ?. subst. by move: Hf Hp'' => ->. ** rewrite Hp''. lia. + rewrite /update Hf. by case: (Nat.eq_dec p p). Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun