Created
March 2, 2020 23:27
-
-
Save bergwerf/c0a811bc6eee2b8f8b37b1044153d673 to your computer and use it in GitHub Desktop.
Spread and fan intersections, which I removed from my intuitionistic math Coq library.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Spread and fan prefix intersections. *) | |
From intuitionism Require Import lib set seq bcp spr fan. | |
(* Finite sequence comparison. *) | |
Section FiniteCompare. | |
(* Check if two sequences have a shared prefix. *) | |
Fixpoint fcompare (s t : fseq) := | |
match s, t with | |
| s1 :: s', t1 :: t' => (s1 =? t1) && fcompare s' t' | |
| _, _ => true | |
end. | |
Lemma fcompare_refl s : fcompare s s = true. | |
Proof. intros; induction s; simpl; auto. repeat bool_to_Prop; auto. Qed. | |
Lemma fcompare_sym s t : | |
fcompare s t = true -> fcompare t s = true. | |
Proof. | |
revert s; induction t; simpl; intros; auto. | |
destruct s; auto; simpl in H. repeat bool_to_Prop; auto. | |
Qed. | |
Lemma fcompare_trans s t u : | |
length t >= length u -> | |
fcompare s t = true -> fcompare t u = true -> fcompare s u = true. | |
Proof. | |
revert s t; induction u; simpl; intros s t. | |
- destruct s, t; simpl; auto. | |
- destruct s, t; simpl; auto; intros L H1 H2. omega. | |
repeat bool_to_Prop. omega. apply IHu with (t:=t0); auto. | |
apply le_S_n; auto. | |
Qed. | |
Lemma fcompare_nil_r s : fcompare s [] = true. | |
Proof. now apply fcompare_sym. Qed. | |
Lemma fcompare_app s t : fcompare s (s ++ t) = true. | |
Proof. induction s; simpl; auto. repeat bool_to_Prop; auto. Qed. | |
Lemma fcompare_app_inv s t u : | |
fcompare s (t ++ u) = true -> fcompare s t = true. | |
Proof. | |
intros; eapply fcompare_trans. 2: apply H. rewrite app_length; omega. | |
apply fcompare_sym; apply fcompare_app. | |
Qed. | |
Lemma fcompare_firstn n s : | |
fcompare s (firstn n s) = true. | |
Proof. | |
revert n; induction s; simpl; auto. destruct n; simpl; auto. | |
repeat bool_to_Prop; auto. | |
Qed. | |
End FiniteCompare. | |
(* Some extra lemmas *) | |
Section Lemmas. | |
Lemma app_nth_firstn (s t : fseq) : | |
length s < length t -> fcompare s t = true | |
-> s ++ [nth (length s) t 0] = firstn (length s + 1) t. | |
Proof. | |
revert t; induction s; simpl; intros. | |
- destruct t0. now simpl in H. easy. | |
- destruct t0; simpl in H. easy. repeat bool_to_Prop; subst. | |
simpl. rewrite IHs; auto. omega. | |
Qed. | |
End Lemmas. | |
(* Spread intersection *) | |
Section SpreadIntersection. | |
Variable X : spread. | |
Variable root : fseq. | |
Variable rootP : σ X root = true. | |
(* Note that get and σ use a reveresed list ordering. *) | |
Definition Iσ s := (fcompare (rev s) (rev root)) && σ X s. | |
Lemma σ_firstn n s : | |
σ X s = true -> σ X (rev (firstn n (rev s))) = true. | |
Proof. | |
induction s; intros. simpl; now rewrite firstn_nil. | |
simpl; rewrite firstn_app; simpl_list. destruct (lt_dec (length s) n) as [N|N]. | |
- replace (n - length s) with (S (n - 1 - length s)) by omega; simpl. | |
rewrite firstn_nil. rewrite firstn_all2; simpl_list. auto. omega. | |
- replace (n - length s) with 0 by omega. rewrite firstn_O, app_nil_r. | |
apply IHs. apply σ_cons. now exists a. | |
Qed. | |
Lemma Iσ_nil : Iσ [] = true. | |
Proof. unfold Iσ; simpl; auto. apply σ_nil. Qed. | |
Lemma Iσ_true s : Iσ s = true -> σ X s = true. | |
Proof. unfold Iσ; intros. now bool_to_Prop. Qed. | |
Lemma Iσ_cons s : Iσ s = true <-> exists n, Iσ (n :: s) = true. | |
Proof. | |
unfold Iσ; simpl; split. | |
- intros; bool_to_Prop. | |
destruct (lt_dec (length (rev s)) (length (rev root))) as [L|L]. | |
+ (* Extend along the root path. *) | |
pose(n := nth (length (rev s)) (rev root) 0). exists n. bool_to_Prop. | |
unfold n; rewrite app_nth_firstn; auto. apply fcompare_sym, fcompare_firstn. | |
replace (n :: s) with (rev ((rev s) ++ [n])) by (simpl_list; auto). | |
unfold n; rewrite app_nth_firstn; auto. apply σ_firstn; auto. | |
+ (* Extend using σ_cons. *) | |
apply σ_cons in H as [n Hn]; exists n. bool_to_Prop; auto. | |
apply fcompare_trans with (t:=rev s); auto. omega. | |
apply fcompare_sym, fcompare_app. | |
- intros [n Hn]; repeat bool_to_Prop. | |
+ apply fcompare_sym; eapply fcompare_app_inv. apply fcompare_sym, Hn0. | |
+ apply σ_cons. exists n; auto. | |
Qed. | |
Definition spread_isect := Spr Iσ Iσ_nil Iσ_cons. | |
End SpreadIntersection. | |
Section FanInterection. | |
Variable F : fan. | |
Variable root : fseq. | |
Variable rootP : σ F root = true. | |
Lemma Iσ_fan s : | |
Iσ F root s = true -> | |
exists n, forall m, Iσ F root (m :: s) = true -> m <= n. | |
Proof. | |
unfold Iσ; intros; bool_to_Prop. apply (fanP F) in H as [n Hn]. | |
exists n; intros; bool_to_Prop; auto. | |
Qed. | |
Definition fan_isect := Fan (spread_isect F root rootP) Iσ_fan. | |
End FanInterection. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment