statement stringlengths 3 176 | proof stringlengths 0 1.55k | type stringclasses 5
values | symbolic_name stringlengths 1 27 | library stringclasses 7
values | filename stringclasses 53
values | imports listlengths 0 0 | deps listlengths 0 13 | docstring stringclasses 1
value | source_url stringclasses 1
value | commit stringclasses 1
value |
|---|---|---|---|---|---|---|---|---|---|---|
hd-wf : [{F:container{i}} {α:choice-sequence(F)} hd(α) ∈ dom(F)] | {
auto; intro @i; auto;
unfold <choice-sequence ν hd>;
elim #1; reduce;
elim #4 [succ(zero)]; reduce; auto;
prune { hyp-subst <- #6 [h.=(dom(h); dom(h); _)]; auto };
@{ [H:extension(_;_) |- _] => elim <H>
}; reduce; auto
}. | theorem | hd-wf | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"choice-sequence",
"dom",
"hd"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
tl-wf : [{F:container{i}} {α:choice-sequence(F)} {p:proj(F; hd(α))} tl(α; p) ∈ choice-sequence(F)] | {
trace "remember to prove tl-wf";
fiat
}. | theorem | tl-wf | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"choice-sequence",
"hd",
"tl"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
chop-prefix : (0;0). | operator | chop-prefix | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[chop-prefix(α; u)] | =def= [
neigh-ind(u; lam(_.α); v.e.ih. lam(z. spread(z; p.p'. tl(ih p; p'))))
]. | definition | chop-prefix | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"tl"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
chop-prefix-wf : [{F:container{i}} {α : choice-sequence(F)} {u:neigh(F)} chop-prefix(α; u) ∈ refinement(F; u) -> choice-sequence(F)] | {
auto;
intro @i; auto; unfold <neighborhoods>; reduce; auto;
unfold <chop-prefix>;
eq-cd [h.refinement(F; h) -> choice-sequence(F), F];
reduce; auto;
[ eq-cd [h.choice-sequence(F)]; auto
, elim #4; reduce; auto; elim #1; reduce; auto
, elim #1; reduce; auto
];
unfold <hd>;
trace "please fix chop... | theorem | chop-prefix-wf | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"choice-sequence",
"chop-prefix",
"hd",
"neighborhoods"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
approximates : (0;0;0). | operator | approximates | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[approximates(F; u; α)] | =def= [
neigh-ind(u; unit; v.e.ih.ih * =(lam(z.hd(chop-prefix(α; v) z)); e; refinement(F; v) -> dom(F)))
]. | definition | approximates | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"chop-prefix",
"dom",
"hd"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
approximates-wf : [{F:container{i}} {u:neigh(F)} {α:choice-sequence(F)} approximates(F; u; α) ∈ U{i}] | {
auto; unfold <neighborhoods>; reduce; auto;
intro @i; auto;
unfold <approximates>;
prune { eq-cd [h.U{i}, F]; auto; };
[ elim #4; reduce; auto; elim #1
, elim #1
, eq-cd [refinement(F; u') -> choice-sequence(F)]; auto;
unfold <neighborhoods>
]; reduce; auto
}. | theorem | approximates-wf | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"approximates",
"choice-sequence",
"neighborhoods"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
approximations : (0;0). | operator | approximations | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[approximations(F; α)] | =def= [{u : neigh(F) | approximates(F; u; α)}]. | definition | approximations | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"approximates"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
approximations-wf : [{F:container{i}} {α:choice-sequence(F)} approximations(F; α) ∈ U{i}] | {
auto; intro @i; auto;
*{ unfold <approximations neighborhoods>; reduce; auto };
}. | theorem | approximations-wf | example/wip/brouwerian | example/wip/brouwerian/choice-sequence.jonprl | [] | [
"approximations",
"choice-sequence",
"neighborhoods"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
finitarily-branching : (0;0). | operator | finitarily-branching | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[finitarily-branching(F;S)] | =def= [
(u : {u : neigh(F) | S u}) is-finite({e : refinement(F; u) -> dom(F) | S (u ^ r. e r)})
]. | definition | finitarily-branching | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [
"dom",
"is-finite"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
finitarily-branching-wf : [{F:container{i}} {S:neigh(F) -> U{i}} finitarily-branching(F; S) ∈ U{i}] | {
auto; unfold <finitarily-branching>; auto; unfold <neighborhoods>; reduce; auto;
elim #1; reduce; auto;
elim #5; elim #6; reduce; auto
}. | theorem | finitarily-branching-wf | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [
"finitarily-branching",
"neighborhoods"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
fan : (0). | operator | fan | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[fan(F)] | =def= [{S:spreiding(F) | finitarily-branching(F; S)}]. | definition | fan | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [
"finitarily-branching",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
fan-wf : [{F:container{i}} fan(F) ∈ U{i'}] | {
auto; unfold <fan>; auto; cum @i; auto;
unfold <spreiding>; auto
}. | theorem | fan-wf | example/wip/brouwerian | example/wip/brouwerian/fan.jonprl | [] | [
"fan",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
[is-hereditary(F; S; Q)] | =def= [
(u:|F ♮|) (e:refinement(F; u) -> |F|) Q (u ^ r. e r) -> Q u
]. | definition | is-hereditary | example/wip/brouwerian | example/wip/brouwerian/generalized-choice-sequences.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
is-hereditary-wf : [{F:container{i}} {S:spreiding(F)} {Q:|F ♮| -> U{i}} is-hereditary(F; S; Q) ∈ U{i}] | {
auto; intro @i'; auto;
unfold <neighborhoods>; reduce; auto;
unfold <is-hereditary>; auto;
unfold <neighborhoods>; reduce; auto;
focus 0 #{ elim #4; reduce; auto };
elim #1; reduce; auto
}. | theorem | is-hereditary-wf | example/wip/brouwerian | example/wip/brouwerian/generalized-choice-sequences.jonprl | [] | [
"is-hereditary",
"neighborhoods",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
[BI-D(F; S; Q; A)] | =def= [
(((u:{u:|F ♮| | S u}) decidable(Q u)) * is-bar(F; S; Q) * is-hereditary(F; S; A) * ((u:|F ♮|) Q u -> A u))
-> A []
]. | definition | BI-D | example/wip/brouwerian | example/wip/brouwerian/generalized-choice-sequences.jonprl | [] | [
"decidable",
"is-bar",
"is-hereditary"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
BI-D-wf : [{F:container{i}} {S:spreiding(F)} {Q:|F ♮| -> U{i}} {A:|F ♮| -> U{i}} BI-D(F; S; Q; A) ∈ U{i}] | {
auto; intro @i'; auto;
unfold <BI-D>; auto;
unfold <spreiding>;
unfold <neighborhoods>; reduce; auto;
eq-cd [neigh(F) -> U{i}]; auto
}. | theorem | BI-D-wf | example/wip/brouwerian | example/wip/brouwerian/generalized-choice-sequences.jonprl | [] | [
"BI-D",
"neighborhoods",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
prefixes : (0;0). | operator | prefixes | example/wip/brouwerian | example/wip/brouwerian/neighborhood.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
10 "≼" := prefixes. | notation | prefixes | example/wip/brouwerian | example/wip/brouwerian/neighborhood.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[u ≼ v] | =def= [neigh-ind(v; neigh-ind(u; unit; _._._.void); w.e.ih.ih)]. | definition | u | example/wip/brouwerian | example/wip/brouwerian/neighborhood.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
prefixes-wf : [{F:container{i}} {u:neigh(F)} {v:neigh(F)} u ≼ v ∈ U{i}] | {
auto; unfold <prefixes neighborhoods>; reduce; auto
}. | theorem | prefixes-wf | example/wip/brouwerian | example/wip/brouwerian/neighborhood.jonprl | [] | [
"neighborhoods",
"prefixes"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
10 "♮" := neighborhoods. | notation | neighborhoods | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
top-wf : [top ∈ U{i}] | {
unfold <top>; auto
}. | theorem | top-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"top"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
ν : (1). | operator | ν | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[ν(x.F[x])] | =def= [{n:nat} natrec(n; top; _.T.F[T])]. | definition | ν | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"top"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
ν-wf : [{F:U{i} -> U{i}} ν(x.F x) ∈ U{i}] | {
auto; unfold <ν>; auto;
}. | theorem | ν-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
decidable : (0). | operator | decidable | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[decidable(P)] | =def= [P + ¬ P]. | definition | decidable | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
not-wf : [{P:U{i}} ¬ P ∈ U{i}] | {
unfold <not>; auto
}. | theorem | not-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"not"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
decidable-wf : [{P:U{i}} decidable(P) ∈ U{i}] | {
unfold <decidable>;
auto
}. | theorem | decidable-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"decidable"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
nat-subtype-base : [{n:nat} n ∈ base] | {
auto; elim #1;
[ auto
, eq-cd; aux { auto };
cstruct; elim #3; auto
]
}. | theorem | nat-subtype-base | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
leq-wf : [{m:nat} {n:nat} (m ≤ n) ∈ U{i}] | {
unfold <leq minus>; auto; wf-lemma <nat-subtype-base>; auto
}. | theorem | leq-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"leq",
"minus",
"nat-subtype-base"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
surj : (0;0;0). | operator | surj | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[surj(A; B; f)] | =def= [(b:B) {a:A | =(f a; b; B)}]. | definition | surj | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
surj-wf : [{A:U{i}} {B:U{i}} {f : A -> B} surj(A; B; f) ∈ U{i}] | {
auto; unfold <surj>; auto
}. | theorem | surj-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"surj"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
is-finite : (0). | operator | is-finite | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[is-finite(A)] | =def= [union(nat; n. {f : upto(n) -> A | surj(upto(n); A; f)})]. | definition | is-finite | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"surj",
"union",
"upto"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
is-finite-wf : [{A:U{i}} is-finite(A) ∈ U{i}] | {
unfold <is-finite union pi2>; auto;
}. | theorem | is-finite-wf | example/wip/brouwerian | example/wip/brouwerian/prolegomenon.jonprl | [] | [
"is-finite",
"pi2",
"union"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-decidable : (0;0). | operator | spw-decidable | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spw-decidable(F; S)] | =def= [(u:neigh(F)) decidable(S u)]. | definition | spw-decidable | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"decidable"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-leaks-upwards : (0;0). | operator | spw-leaks-upwards | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spw-leaks-upwards(F; S)] | =def= [(u:neigh(F)) S u -> (e:proj(F ♮; u) -> dom(F)) * S (u ^ r. e r)]. | definition | spw-leaks-upwards | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"dom"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-downward-closed : (0;0). | operator | spw-downward-closed | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spw-downward-closed(F; S)] | =def= [(v:neigh(F)) (u:{u : neigh(F) | u ≼ v}) S u -> S v]. | definition | spw-downward-closed | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-decidable-wf : [{F:container{i}} {S:neigh(F) -> U{i}} spw-decidable(F; S) ∈ U{i}] | {
unfold <spw-decidable neighborhoods>; reduce; auto;
elim #1; auto
}. | theorem | spw-decidable-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"neighborhoods",
"spw-decidable"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-leaks-upwards-wf : [{F:container{i}} {S:neigh(F) -> U{i}} spw-leaks-upwards(F; S) ∈ U{i}] | {
unfold <spw-leaks-upwards neighborhoods>; reduce; auto;
elim #1; auto; reduce; auto;
elim #5; reduce; auto
}. | theorem | spw-leaks-upwards-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"neighborhoods",
"spw-leaks-upwards"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spw-downward-closed-wf : [{F:container{i}} {S:neigh(F) -> U{i}} spw-downward-closed(F; S) ∈ U{i}] | {
auto; unfold <spw-downward-closed neighborhoods>; reduce; auto;
cut-lemma <prefixes-wf>;
elim #5 [F]; auto;
unfold <member neighborhoods>; reduce;
bhyp #6; auto;
}. | theorem | spw-downward-closed-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"member",
"neighborhoods",
"prefixes-wf",
"spw-downward-closed"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spreidingswet : (0;0). | operator | spreidingswet | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spreidingswet(F; S)] | =def= [
spw-decidable(F; S)
* spw-leaks-upwards(F; S)
* spw-downward-closed(F; S)
* S []
]. | definition | spreidingswet | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"spw-decidable",
"spw-downward-closed",
"spw-leaks-upwards"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spreidingswet-wf : [{F:container{i}} {S:neigh(F) -> U{i}} spreidingswet(F;S) ∈ U{i}] | {
intro @i'; aux { auto };
intro @i'; aux { elim #1; auto };
auto; *{ unfold <spreidingswet neighborhoods>; reduce; auto }
}. | theorem | spreidingswet-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"neighborhoods",
"spreidingswet"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spreiding : (0). | operator | spreiding | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spreiding(F)] | =def= [{S:neigh(F) -> U{i} | spreidingswet(F; S)}]. | definition | spreiding | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"spreidingswet"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spreiding-wf : [{F:container{i}} spreiding(F) ∈ U{i'}] | {
auto; unfold <spreiding neighborhoods>; reduce; auto;
cum @i; auto; unfold <neighborhoods>; reduce; auto
}. | theorem | spreiding-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"neighborhoods",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
universal-spread : (). | operator | universal-spread | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[universal-spread] | =def= [lam(_.unit)]. | definition | universal-spread | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
universal-spread-pre-wf : [{F:container{i}} universal-spread ∈ neigh(F) -> U{i}] | {
auto; unfold <universal-spread neighborhoods>; auto;
elim #1; reduce; auto
}. | theorem | universal-spread-pre-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"neighborhoods",
"universal-spread"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
universal-spread-wf : [{F:container{i}} (s:dom(F)) universal-spread ∈ spreiding(F)] | {
unfold <spreiding>; auto; aux { elim #1; reduce; auto };
eq-cd @i; ?{ !{ auto } };
unfold <spreidingswet>; auto;
unfold <neighborhoods>; reduce; auto;
unfold <universal-spread>; reduce; auto;
aux { elim #3; reduce; auto; elim #1; reduce; auto };
focus 0 #{ intro #0; auto };
intro @i; auto;
cut-lemma... | theorem | universal-spread-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"dom",
"member",
"neighborhoods",
"prefixes-wf",
"spreiding",
"spreidingswet",
"universal-spread"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spread-extension : (0;0). | operator | spread-extension | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | ||
[spread-extension(F; S)] | =def= [{α:choice-sequence(F) | (u:approximations(F; α)) S u}]. | definition | spread-extension | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"approximations",
"choice-sequence"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
spread-extension-wf : [{F:container{i}} {S : spreiding(F)} spread-extension(F; S) ∈ U{i}] | {
auto; intro @i'; auto;
unfold <spread-extension>; auto;
unfold <spreiding>;
elim #2; unfold <approximations neighborhoods>; reduce; auto
}. | theorem | spread-extension-wf | example/wip/brouwerian | example/wip/brouwerian/spread.jonprl | [] | [
"approximations",
"neighborhoods",
"spread-extension",
"spreiding"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
squash-intro | {
@{
[|- squash(A)] =>
assert [A];
focus 1 #{
@{
[H : A |- _] =>
unfold <squash member>; witness [lam(_.<>) H]; auto
}
}
}
}. | tactic | squash-intro | stdlib | stdlib/tactics.jonprl | [] | [
"assert",
"member",
"squash"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
contradiction | {
@{ [H:P, H':not(P) |- _] => unfold <not implies>; elim <H'> [H]; auto
| [H:P, H':P -> void |- _] => elim <H'> [H]; auto
| [H:P, H':P => void |- _] => elim <H'> [H]; auto
}
}. | tactic | contradiction | stdlib | stdlib/tactics.jonprl | [] | [
"implies",
"not"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
bunion-eq-right | {
@{ [|- =(M; N; bunion(L; R))] =>
csubst [ceq(M; lam(x. snd(x)) <inr(<>), M>)] [h.=(h;_;_)];
aux { unfold <snd>; reduce; auto };
csubst [ceq(N; lam(x. snd(x)) <inr(<>), N>)] [h.=(_;h;_)];
aux { unfold <snd>; reduce; auto };
unfold <bunion>; eq-cd; auto; reduce;
aux {
... | tactic | bunion-eq-right | stdlib | stdlib/tactics.jonprl | [] | [
"bunion",
"ceq",
"snd"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
bunion-eq-left | {
@{ [|- =(M; N; bunion(L; R))] =>
csubst [ceq(M; lam(x. snd(x)) <inl(<>), M>)] [h.=(h;_;_)];
aux { unfold <snd>; reduce; auto };
csubst [ceq(N; lam(x. snd(x)) <inl(<>), N>)] [h.=(_;h;_)];
aux { unfold <snd>; reduce; auto };
unfold <bunion>; eq-cd; auto; reduce;
aux {
... | tactic | bunion-eq-left | stdlib | stdlib/tactics.jonprl | [] | [
"bunion",
"ceq",
"snd"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
eq-base-tac | {
@{ [|- =(=(_; _; _); =(_; _; _); _)] =>
eq-eq-base; ?{ !{ bunion-eq-right; auto } }
| [|- =(_ * _; _ * _; _)] => eq-cd
| [|- =(_ => _; _ => _; _)] => eq-cd
| [|- =(_ -> _; _ -> _; _)] => eq-cd
| [|- member(_; _)] => unfold <member>
}
}. | tactic | eq-base-tac | stdlib | stdlib/tactics.jonprl | [] | [
"bunion-eq-right",
"member"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
destruct-prods | {
*{ @{ [H:_*_ |- _] => elim <H>; thin <H>
}
}
}. | tactic | destruct-prods | stdlib | stdlib/tactics.jonprl | [] | [] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 | |
hyp-trans | {
@{ [H : P, H' : P => Q, H'' : Q => R |- R] =>
assert [Q] <z>;
aux {
elim <H'> [H]; auto
};
main {
elim <H''> [z];
auto
}
| [H : P, H' : P => Q |- Q] =>
elim <H'> [H]; auto
}
}. | tactic | hyp-trans | stdlib | stdlib/tactics.jonprl | [] | [
"assert"
] | https://github.com/jonsterling/JonPRL | f937a5461955fff8cb22331ecb6fdeae8df636d5 |
Subsets and Splits
No community queries yet
The top public SQL queries from the community will appear here once available.