summaryrefslogtreecommitdiff
path: root/support/proof/example.mp
blob: ab38972393c141503bf06c6730aef7d8fccf1351 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
% Sample MetaPost sourcefile ()


beginfig(1);
a=.7in; b=0.5in;
z0=(0,0); z1=(a,0); z2=(0,b);
z0=.5[z1,z3]=.5[z2,z4];
draw z1..z2..z3..z4..cycle;
drawarrow z0..z1;
drawarrow z0..z2;
label.top(btex $a$ etex, .5[z0,z1]);
label.lft(btex $b$ etex, .5[z0,z2]);
endfig;


beginfig(2);

h=2in; w=2.7in;
path p[], q[], pp;
for i=1.5,2,4:
  ii := i**2;
  p[i] = (w/ii,h){1/ii,-1}...(w/i,h/i)...(w,h/ii){1,-1/ii};
endfor
for i=.5,1.5:
  q[i] = origin..(w,i*h) cutafter p1.5;
endfor

pp = buildcycle(q0.5, p2, q1.5, p4);

fill pp withcolor .8white;
z0=center pp;
picture lab; lab=thelabel(btex $f>0$ etex, z0);
unfill bbox lab; draw lab;
draw q0.5; draw p2; draw q1.5; draw p4;
makelabel.top(btex $P$ etex, p2 intersectionpoint q0.5);
makelabel.rt(btex $Q$ etex, p2 intersectionpoint q1.5);
endfig;


beginfig(3);

3.2scf = 2.4in;
path fun;
# = .1;  % Keep the function single-valued
fun = ((0,-1#)..(1,.5#){right}..(1.9,.2#){right}..{curl .1}(3.2,2#))
  scaled scf yscaled(1/#);

vardef vertline primary x = (x,-infinity)..(x,infinity) enddef;
primarydef f atx x = (f intersectionpoint vertline x) enddef;
primarydef f whenx x = xpart(f intersectiontimes vertline x) enddef;

z1a = (2.5scf,0);
z1 = fun atx x1a;
y2a=0; z1-z2a=whatever*direction fun whenx x1 of fun;
z2 = fun atx x2a;
y3a=0; z2-z3a=whatever*direction fun whenx x2 of fun;

draw fun withpen pencircle scaled 1pt;
drawarrow (0,0)..(3.2scf,0);

label.bot(btex $x_1$ etex, z1a);
draw z1a..z1 dashed evenly;
makelabel(nullpicture, z1);
draw z1..z2a withpen pencircle scaled .3;
label.bot(btex $x_2$ etex, z2a);
draw z2a..z2 dashed evenly;
makelabel(nullpicture, z2);
draw z2..z3a withpen pencircle scaled .3;
label.bot(btex $x_3$ etex, z3a);
endfig;


beginfig(4);
for i=0 upto 2:
  z[i]=(0,40i); z[i+3]-z[i]=(100,30);
endfor
pickup pencircle scaled 18;
def gray = withcolor .8white enddef;
draw z0..z3 gray;
linecap:=butt; draw z1..z4 gray;
linecap:=squared; draw z2..z5 gray;
labels.top(0,1,2,3,4,5);
endfig; linecap:=rounded;

end