Skip to content

Instantly share code, notes, and snippets.

@vlj

vlj/ring2.v

Last active April 4, 2020 01:23
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save vlj/caebeb393abf76342a409d871ed39a86 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save vlj/caebeb393abf76342a409d871ed39a86 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. vlj renamed this gist Mar 31, 2020. 1 changed file with 0 additions and 0 deletions.
    0 ring2 → ring2.v
    View file
    File renamed without changes.
  2. vlj created this gist Mar 31, 2020.
    34 changes: 34 additions & 0 deletions ring2
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,34 @@
    From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
    Require Import Ring.

    Open Scope ring_scope.

    Import GRing.Theory.

    Variable R: numFieldType.

    Definition rt :
    @ring_theory R 0%:R 1%:R +%R *%R (fun a b => a - b) -%R eq.
    Proof.
    apply mk_rt.
    apply add0r.
    apply addrC.
    apply addrA.
    apply mul1r.
    apply mulrC.
    apply mulrA.
    apply mulrDl.
    by [].
    apply subrr.
    Qed.


    Add Ring Ringgg : rt.

    Lemma tmp2:
    forall x y z:R, x + y = y + x.
    Proof.
    move => x y z.
    Unset Printing Notations.
    Fail ring_simplify.
    Qed.