Conversation
| { | ||
| sublist₁ := show [] <+ [] from .slnil | ||
| sublist₂ := show [] <+ ys from ys.nil_sublist | ||
| longest | ||
| | cs, ⟨(h : cs <+ []), _⟩ => | ||
| show cs.length ≤ [].length from | ||
| suffices cs = [] from this.rec Nat.le.refl | ||
| eq_nil_of_sublist_nil h | ||
| } |
There was a problem hiding this comment.
Usually we would format this as
| { | |
| sublist₁ := show [] <+ [] from .slnil | |
| sublist₂ := show [] <+ ys from ys.nil_sublist | |
| longest | |
| | cs, ⟨(h : cs <+ []), _⟩ => | |
| show cs.length ≤ [].length from | |
| suffices cs = [] from this.rec Nat.le.refl | |
| eq_nil_of_sublist_nil h | |
| } | |
| { sublist₁ := show [] <+ [] from .slnil | |
| sublist₂ := show [] <+ ys from ys.nil_sublist | |
| longest | |
| | cs, ⟨(h : cs <+ []), _⟩ => | |
| show cs.length ≤ [].length from | |
| suffices cs = [] from this.rec Nat.le.refl | |
| eq_nil_of_sublist_nil h } |
(and throughout)
| /-- `cs` is a common sublist of the lists `xs` and `ys`. -/ | ||
| public structure CommonSublist (xs ys cs : List α) : Prop where |
There was a problem hiding this comment.
| /-- `cs` is a common sublist of the lists `xs` and `ys`. -/ | |
| public structure CommonSublist (xs ys cs : List α) : Prop where | |
| /-- `IsCommonSublist xs ys xs` indicates that `cs` is a common sublist of the lists `xs` and `ys`. -/ | |
| public structure IsCommonSublist (xs ys cs : List α) : Prop where |
There was a problem hiding this comment.
You might want to put the cs argument first so that you can write cs.IsCommonSublist xs ys too
| theorem nil_lcsBrute : {ys : List α} → lcsBrute [] ys = [] | ||
| | [] | _ :: _ => lcsBrute.eq_def .. | ||
|
|
||
| theorem lcsBrute_nil : {xs : List α} → lcsBrute xs [] = [] | ||
| | [] | _ :: _ => lcsBrute.eq_def .. |
There was a problem hiding this comment.
These should be @[simp]
| | [] | _ :: _ => lcsBrute.eq_def .. | ||
|
|
||
| theorem lcsBrute_correct : {xs ys : List α} → LCS xs ys (lcsBrute xs ys) | ||
| | [], ys => |
There was a problem hiding this comment.
Instead of doing a manual pattern match here, I think it would be better to use fun_induction, which will aso handle the x = y case split for you.
There was a problem hiding this comment.
Also, I am pretty sure simp could handle this case, maybe with some sublist lemmas. Especially if you follow my Prop def suggestion.
| aux3 (x : α) : α × DP α → DPS α × DP α × DP α → TimeM ℕ (DPS α × DP α × DP α) | ||
| | (y, xx), (dps, yy, xy) => do | ||
| ✓ let dp := dp x y xx yy xy | ||
| return ((y, dp) :: dps, dp, xx) | ||
| dp (x y : α) (xx yy xy : DP α) : DP α := | ||
| if x = y then | ||
| ⟨x :: xy.lcs, xy.length + 1, xy.length_eq.rec rfl⟩ | ||
| else | ||
| if xx.length ≥ yy.length then xx else yy |
There was a problem hiding this comment.
I'd suggest
| aux3 (x : α) : α × DP α → DPS α × DP α × DP α → TimeM ℕ (DPS α × DP α × DP α) | |
| | (y, xx), (dps, yy, xy) => do | |
| ✓ let dp := dp x y xx yy xy | |
| return ((y, dp) :: dps, dp, xx) | |
| dp (x y : α) (xx yy xy : DP α) : DP α := | |
| if x = y then | |
| ⟨x :: xy.lcs, xy.length + 1, xy.length_eq.rec rfl⟩ | |
| else | |
| if xx.length ≥ yy.length then xx else yy | |
| aux3 (x : α) : α × DP α → DPS α × DP α × DP α → TimeM ℕ (DPS α × DP α × DP α) | |
| | (y, xx), (dps, yy, xy) => do | |
| let dp ← dp x y xx yy xy | |
| return ((y, dp) :: dps, dp, xx) | |
| dp (x y : α) (xx yy xy : DP α) : TimeM (DP α) := do | |
| ✓ if x = y then | |
| return ⟨x :: xy.lcs, xy.length + 1, xy.length_eq.rec rfl⟩ | |
| else | |
| return if xx.length ≥ yy.length then xx else yy |
| @@ -0,0 +1,354 @@ | |||
| module | |||
|
|
|||
There was a problem hiding this comment.
you might want to put @[expose] public section here. This exposes all your definitions by default.
| variable {α} [DecidableEq α] | ||
|
|
||
| /-- `cs` is a common sublist of the lists `xs` and `ys`. -/ | ||
| public structure CommonSublist (xs ys cs : List α) : Prop where |
There was a problem hiding this comment.
Explicit public is not required.
| variable {α} [DecidableEq α] | ||
|
|
||
| /-- `cs` is a common sublist of the lists `xs` and `ys`. -/ | ||
| public structure CommonSublist (xs ys cs : List α) : Prop where |
There was a problem hiding this comment.
Also why not just
abbrev CommonSublist (xs ys cs : List α) : Prop := (cs <+ xs) ∧ (cs <+ ys)
?
| sublist₂ : cs <+ ys | ||
|
|
||
| /-- `lcs` is a longest common sublist of the lists `xs` and `ys`. -/ | ||
| public structure LCS (xs ys lcs : List α) : Prop extends CommonSublist xs ys lcs where |
There was a problem hiding this comment.
Following my suggestion on CommonSubList, this could just be
abbrev LCS (xs ys lcs : List α) := CommonSubList xs ys lcs ∧ ∀ cs, CommonSublist xs ys cs → cs.length ≤ lcs.length
| | [] | _ :: _ => lcsBrute.eq_def .. | ||
|
|
||
| theorem lcsBrute_correct : {xs ys : List α} → LCS xs ys (lcsBrute xs ys) | ||
| | [], ys => |
There was a problem hiding this comment.
Also, I am pretty sure simp could handle this case, maybe with some sublist lemmas. Especially if you follow my Prop def suggestion.
|
|
||
| namespace lcsDP | ||
|
|
||
| structure DP α where |
There was a problem hiding this comment.
For LCS you should really just take the list length as an input parameter. Even better, solve for a general l which denotes a prefix of the list (including the whole list if l \geq n) to an auxiliary function, and then pass List.length as the argument to this parameter in the actual function
|
|
||
| scoped instance : Inhabited (DP α) where default := ⟨[], 0, rfl⟩ | ||
| example : @Eq (DP α) default ⟨[], 0, rfl⟩ := rfl | ||
| abbrev DPS α := List (α × DP α) |
There was a problem hiding this comment.
why this second definition at all?
| else | ||
| if xx.length ≥ yy.length then xx else yy | ||
|
|
||
| section unittest |
There was a problem hiding this comment.
This entire section goes in the CslibTests folder. Please don't put tests in the main library folder.
|
|
||
| variable {x y : α} {xs ys : List α} | ||
|
|
||
| theorem cons_aux0 : ⟪aux0 (x :: xs) ys⟫ = ⟪aux1 x ⟪aux0 xs ys⟫⟫ := |
There was a problem hiding this comment.
The four lemmas about aux0 sound like things you will get free as equational lemmas from lean. You should probably just fun_induction wherever you use these lemmas. I could be wrong so I'll tag @eric-wieser to check. If these lemmas stay, they probably ought to be @[simp]
3 participants
Time complexity using
TimeMis proven, butTimeMis messing up my lemmasaux2_1andcons_aux0_consfor the correctness prooflcsDPwhereas my original non-monadic implementation can utilize definitional equality ofList.foldr. Reviewers can start giving feedback while I work on the 2 lemmas withsorry.