<filename>zulip_json/113488-general/structure.20equality.json
[
    {
        "content": "<p>How do we prove equality of two terms whose type is a structure mixing data and Prop? I would like to prove each data holding field matches. I thought this has something to do with <code>no_confusion</code> but I can't get it to work.</p>",
        "id": 129218426,
        "sender_full_name": "<NAME>",
        "timestamp": 1530903334
    },
    {
        "content": "<p>Hum, it seems I can uses cases to access stuff here again.</p>",
        "id": 129218697,
        "sender_full_name": "<NAME>",
        "timestamp": 1530903665
    },
    {
        "content": "<div class=\"codehilite\"><pre><span></span><span class=\"kn\">structure</span> <span class=\"n\">thing</span> <span class=\"o\">:=</span> <span class=\"o\">(</span><span class=\"n\">a</span> <span class=\"o\">:</span> <span class=\"bp\">ℕ</span><span class=\"o\">)</span> <span class=\"o\">(</span><span class=\"n\">b</span> <span class=\"o\">:</span> <span class=\"bp\">ℕ</span><span class=\"o\">)</span>\n\n<span class=\"kn\">example</span> <span class=\"o\">(</span><span class=\"n\">a</span> <span class=\"n\">b</span> <span class=\"n\">c</span> <span class=\"n\">d</span> <span class=\"o\">:</span> <span class=\"bp\">ℕ</span><span class=\"o\">)</span> <span class=\"o\">:</span> <span class=\"n\">thing</span><span class=\"bp\">.</span><span class=\"n\">mk</span> <span class=\"n\">a</span> <span class=\"n\">b</span> <span class=\"bp\">=</span> <span class=\"n\">thing</span><span class=\"bp\">.</span><span class=\"n\">mk</span> <span class=\"n\">c</span> <span class=\"n\">d</span> <span class=\"o\">:=</span>\n<span class=\"k\">begin</span>\n   <span class=\"n\">rw</span> <span class=\"n\">thing</span><span class=\"bp\">.</span><span class=\"n\">mk</span><span class=\"bp\">.</span><span class=\"n\">inj_eq</span><span class=\"o\">,</span>\n<span class=\"kn\">end</span>\n</pre></div>\n\n\n<p><code>simp</code> also works.</p>",
        "id": 129218843,
        "sender_full_name": "<NAME>",
        "timestamp": 1530903829
    },
    {
        "content": "<p>I'm not sure what to do if you haven't done cases.</p>",
        "id": 129218950,
        "sender_full_name": "<NAME>",
        "timestamp": 1530903915
    },
    {
        "content": "<p>You can also use <code>congr</code> or <code>congr'</code></p>",
        "id": 129219284,
        "sender_full_name": "<NAME>",
        "timestamp": 1530904394
    },
    {
        "content": "<p>What's the difference between <code>congr</code> and <code>congr'</code>?</p>",
        "id": 129219344,
        "sender_full_name": "<NAME>",
        "timestamp": 1530904457
    },
    {
        "content": "<p><code>congr'</code> takes an argument like <code>congr' 3</code> to ask for three iterations of congruence. <code>congr</code> just keeps going until it can't anymore. Often, <code>congr</code> goes too far</p>",
        "id": 129219395,
        "sender_full_name": "<NAME>udon",
        "timestamp": 1530904546
    },
    {
        "content": "<p>Thanks Chris and Simon. <code>congr</code> and <code>simp</code> do nothing, <code>cases</code> both sides and <code>rw pequiv.mk.inj_eq ; cc</code> did the trick</p>",
        "id": 129221654,
        "sender_full_name": "<NAME>",
        "timestamp": 1530907427
    },
    {
        "content": "<p>Sorry, I didn't mention, in either case, you need to <code>cases</code> both sides</p>",
        "id": 129221846,
        "sender_full_name": "<NAME>",
        "timestamp": 1530907593
    },
    {
        "content": "<p>Correction, after cases both sides, <code>congr ; cc</code> also works</p>",
        "id": 129222086,
        "sender_full_name": "<NAME>",
        "timestamp": 1530907901
    },
    {
        "content": "<p>and <code>congr ; tauto</code> of course</p>",
        "id": 129222164,
        "sender_full_name": "<NAME>",
        "timestamp": 1530907976
    },
    {
        "content": "<p>I'm wrapping up a round of optimization of <code>tauto</code>. When it works, it should be faster than <code>cc</code></p>",
        "id": 129222707,
        "sender_full_name": "<NAME>",
        "timestamp": 1530908555
    },
    {
        "content": "<p>(and now, it should work more often than before)</p>",
        "id": 129222733,
        "sender_full_name": "<NAME>",
        "timestamp": 1530908601
    },
    {
        "content": "<p>Great!</p>",
        "id": 129222738,
        "sender_full_name": "<NAME>",
        "timestamp": 1530908611
    }
]