verification/verifier2.html at master · iposov/verification · GitHub

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
87
<!DOCTYPE HTML>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width">
    <title>Verification</title>
    <script src="https://sagecell.sagemath.org/static/embedded_sagecell.js"></script>
    <script>
    sagecell.makeSagecell({inputLocation:  '#verification-template',
                           template:       sagecell.templates.minimal,
                           autoeval: true,
                           hide: ["evalButton"]
    });
    </script>
  </head>
  <body>

    <div id="verification-template">
    <script type="text/x-sage">
from sage.misc.html import HtmlFragment
from sage.interfaces.qepcad import qformula

def verifier_task_qe(statement, show_example, teacher_formula, vars, qvars):
    show_text(statement)

    show_text(r"Use <tt>/\</tt>, <tt>\/</tt>, <tt>~</tt>, <tt>==></tt>, <tt><==></tt> as logical operators, <tt>&gt;</tt>, <tt>&gt;=</tt>, <tt>&lt;</tt>, <tt>&lt;=</tt>, <tt>=</tt>, <tt>/=</tt> as comparison operators.")

    @interact
    def _(ans=input_box(default=r"a + b + c < 0", label="Your answer", type=str)):
        teacher_formula_wrapped = qformula(teacher_formula, frozenset(vars), list(qvars))
        teacher_formula_simplified = qepcad(teacher_formula_wrapped)

        ans = ans.replace('(', '[').replace(')', ']')

        refuter_formula = fr'[[~[{teacher_formula_simplified}]] /\ [{ans}]]'
        complementer_formula = fr'[[{teacher_formula_simplified}] /\ [~[{ans}]]]'

        refuter_formula_wrapped=qformula(refuter_formula, vars=frozenset(vars))
        refuter_formula_simplified = qepcad(refuter_formula_wrapped)
        complementer_formula_wrapped=qformula(complementer_formula, vars=frozenset(vars))
        complementer_formula_simplified = qepcad(complementer_formula_wrapped)

        has_refuting = refuter_formula_simplified != "FALSE"
        has_complementer = complementer_formula_simplified != "FALSE"

        if has_refuting or has_complementer:
            show_text("Your answer is wrong,")
            if has_refuting:
                show_text("the following example refutes it:")
                refuter_test = qepcad(refuter_formula_wrapped, solution='any-point')
                show_example(**refuter_test)

            if has_complementer:
                show_text("the following example complements it:")
                complementer_test = qepcad(complementer_formula_wrapped, solution='any-point')
                show_example(**complementer_test)
        else:
          show_text("You are correct!")


def show_example(a, b, c):
    var('a,b,c,x')
    f(x) = a*x^2 + b*x + c
    show("f(x) = " + latex(f(x)))
    show(plot(f(x), (x, -5, 5), figsize=[2, 2]))

def show_text(text):
    show(HtmlFragment(text))

teacher_formula = "(A x) [[x <= 0] ==> [a x^2 + b x + c < 0]]"
vars = 'abc'  # free variables go first
qvars = 'x'

verifier_task_qe(
  "In what conditions on $a$, $b$, $c$ the function $f(x) = ax^2+bx+c$ does not intersect the second quarter?",
  show_example,
  teacher_formula,
  vars,
  qvars
)


    </script>
    </div>

  </body>
</html>