Skip to content

Commit

Permalink
Fix proof so Coq 8.18 doesn't complain
Browse files Browse the repository at this point in the history
  • Loading branch information
huynhtrankhanh committed Mar 2, 2024
1 parent 52c0c23 commit 976dd96
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions theories/RegularBracketString.v
Original file line number Diff line number Diff line change
@@ -316,7 +316,7 @@ Proof.
assert (H2 : BracketOpen :: s `prefix_of` BracketOpen :: s ++ [BracketOpen]).
{ exists [BracketOpen]. easy. }
pose proof h1 (BracketOpen :: s) H2 as H0. autorewrite with rewriteCount in H0. lia. }
{ reflexivity. }
{ rewrite firstn_all, Nat.sub_diag. simpl. now rewrite app_nil_r. }
+ destruct h as [_ h].
pose proof h [BracketClose] as H0.
assert (H2 : [BracketClose] `prefix_of` BracketClose :: s).
@@ -351,7 +351,7 @@ Proof.
{ apply prefix_cons, prefix_app_r. assumption. }
pose proof h2 (BracketOpen :: prefix) H4 as H6. autorewrite with rewriteCount in H6.
assert (H5 : take (length prefix) (w ++ [BracketClose]) = prefix).
{ destruct h as [w1 h]. rewrite h, <- app_assoc, take_app. reflexivity. }
{ destruct h as [w1 h]. rewrite h, <- app_assoc, take_app, Nat.sub_diag, firstn_all, firstn_O, app_nil_r. reflexivity. }
rewrite H5 in *.
lia. }
assert (H2 : balanceFactorBasedDefinition w). { split; assumption. }

0 comments on commit 976dd96

Please sign in to comment.