Splitting disjunctions (/) in Coq hypothesisProving if then else in CoqHow to apply a Coq hypothesis of the form A = B -> C = D to a subgoal of the form A = BCoq - Error when eliminating ORWhat forms of goal in Coq are considered to be “true”?“Rewrite” a typeHow to make Coq evaluate a specific redex (or - why does it refuse in this case?)How to destruct pair equivalence in Coq?Rewrite hypothesis in Coq, keeping implicationCoq: Rewriting with 'forall' in hypothesis or goalNon-empty list append theorem in Coq

Is CD audio quality good enough for the final delivery of music?

What do different value notes on the same line mean?

Four-in-a-line Puzzle

How do you say “buy” in the sense of “believe”?

Does this degree 12 genus 1 curve have only one point over infinitely many finite fields?

Why colon to denote that a value belongs to a type?

Does revoking a certificate result in revocation of its key?

How many chess players are over 2500 Elo?

Why does the 'metric Lagrangian' approach appear to fail in Newtonian mechanics?

Seed ship, unsexed person, cover has golden person attached to ship by umbilical cord

Would jet fuel for an F-16 or F-35 be producible during WW2?

How were these pictures of spacecraft wind tunnel testing taken?

Placing bypass capacitors after VCC reaches the IC

Is the first derivative operation on a signal a causal system?

General purpose replacement for enum with FlagsAttribute

When and what was the first 3D acceleration device ever released?

How can people dance around bonfires on Lag Lo'Omer - it's darchei emori?

What is the object moving across the ceiling in this stock footage?

Logarithm of dependent variable is uniformly distributed. How to calculate a confidence interval for the mean?

Employer demanding to see degree after poor code review

Where is the logic in castrating fighters?

Full horizontal justification in table

How did early x86 BIOS programmers manage to program full blown TUIs given very few bytes of ROM/EPROM?

Rename photos to match video titles



Splitting disjunctions (/) in Coq hypothesis


Proving if then else in CoqHow to apply a Coq hypothesis of the form A = B -> C = D to a subgoal of the form A = BCoq - Error when eliminating ORWhat forms of goal in Coq are considered to be “true”?“Rewrite” a typeHow to make Coq evaluate a specific redex (or - why does it refuse in this case?)How to destruct pair equivalence in Coq?Rewrite hypothesis in Coq, keeping implicationCoq: Rewriting with 'forall' in hypothesis or goalNon-empty list append theorem in Coq






.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty height:90px;width:728px;box-sizing:border-box;








1















I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
but can't manage to split them when they appear in the hypothesis. Here is my example:



Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
 ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
 intros n H1.
 split H1. (** this doesn't work ... *)


And here is what Coq says:



1 subgoal
n : nat
H1 : n < 5 / n > 8
______________________________________(1/1)
n > 7 / n < 6


With error:



Error: Illegal tactic application.


I'm clearly missing something simple.
Any help is very much appreciated, thanks!






coq







share|improve this question




























    1















    I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
    but can't manage to split them when they appear in the hypothesis. Here is my example:



    Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
     ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
    Proof.
     intros n H1.
     split H1. (** this doesn't work ... *)


    And here is what Coq says:



    1 subgoal
    n : nat
    H1 : n < 5 / n > 8
    ______________________________________(1/1)
    n > 7 / n < 6


    With error:



    Error: Illegal tactic application.


    I'm clearly missing something simple.
    Any help is very much appreciated, thanks!






    coq







    share|improve this question
























      1












      1








      1








      I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
      but can't manage to split them when they appear in the hypothesis. Here is my example:



      Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
       ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
      Proof.
       intros n H1.
       split H1. (** this doesn't work ... *)


      And here is what Coq says:



      1 subgoal
      n : nat
      H1 : n < 5 / n > 8
      ______________________________________(1/1)
      n > 7 / n < 6


      With error:



      Error: Illegal tactic application.


      I'm clearly missing something simple.
      Any help is very much appreciated, thanks!






      coq







      share|improve this question














      I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
      but can't manage to split them when they appear in the hypothesis. Here is my example:



      Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
       ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
      Proof.
       intros n H1.
       split H1. (** this doesn't work ... *)


      And here is what Coq says:



      1 subgoal
      n : nat
      H1 : n < 5 / n > 8
      ______________________________________(1/1)
      n > 7 / n < 6


      With error:



      Error: Illegal tactic application.


      I'm clearly missing something simple.
      Any help is very much appreciated, thanks!






      coq




      coq






      share|improve this question













      share|improve this question











      share|improve this question




      share|improve this question










      asked Mar 24 at 6:38









      OrenIshShalomOrenIshShalom

      1,239924




      1,239924






















          1 Answer
          1






          active

          oldest

          votes


















          2














          The tactic you want is destruct.



          Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
           ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
          Proof.
           intros n H1.
           destruct H1.


          If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..






          share|improve this answer























            Your Answer






            StackExchange.ifUsing("editor", function ()
            StackExchange.using("externalEditor", function ()
            StackExchange.using("snippets", function ()
            StackExchange.snippets.init();
            );
            );
            , "code-snippets");

            StackExchange.ready(function()
            var channelOptions =
            tags: "".split(" "),
            id: "1"
            ;
            initTagRenderer("".split(" "), "".split(" "), channelOptions);

            StackExchange.using("externalEditor", function()
            // Have to fire editor after snippets, if snippets enabled
            if (StackExchange.settings.snippets.snippetsEnabled)
            StackExchange.using("snippets", function()
            createEditor();
            );

            else
            createEditor();

            );

            function createEditor()
            StackExchange.prepareEditor(
            heartbeatType: 'answer',
            autoActivateHeartbeat: false,
            convertImagesToLinks: true,
            noModals: true,
            showLowRepImageUploadWarning: true,
            reputationToPostImages: 10,
            bindNavPrevention: true,
            postfix: "",
            imageUploader:
            brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
            contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
            allowUrls: true
            ,
            onDemand: true,
            discardSelector: ".discard-answer"
            ,immediatelyShowMarkdownHelp:true
            );



            );













            draft saved

            draft discarded


















            StackExchange.ready(
            function ()
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55321328%2fsplitting-disjunctions-in-coq-hypothesis%23new-answer', 'question_page');

            );

            Post as a guest















            Required, but never shown

























            1 Answer
            1






            active

            oldest

            votes








            1 Answer
            1






            active

            oldest

            votes









            active

            oldest

            votes






            active

            oldest

            votes









            2














            The tactic you want is destruct.



            Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
             ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
            Proof.
             intros n H1.
             destruct H1.


            If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..






            share|improve this answer



























              2














              The tactic you want is destruct.



              Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
               ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
              Proof.
               intros n H1.
               destruct H1.


              If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..






              share|improve this answer

























                2












                2








                2







                The tactic you want is destruct.



                Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
                 ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
                Proof.
                 intros n H1.
                 destruct H1.


                If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..






                share|improve this answer













                The tactic you want is destruct.



                Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
                 ((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
                Proof.
                 intros n H1.
                 destruct H1.


                If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..







                share|improve this answer












                share|improve this answer



                share|improve this answer










                answered Mar 24 at 7:30









                UserUser

                1,8391710




                1,8391710





























                    draft saved

                    draft discarded
















































                    Thanks for contributing an answer to Stack Overflow!


                    • Please be sure to answer the question. Provide details and share your research!

                    But avoid …


                    • Asking for help, clarification, or responding to other answers.

                    • Making statements based on opinion; back them up with references or personal experience.

                    To learn more, see our tips on writing great answers.




                    draft saved


                    draft discarded














                    StackExchange.ready(
                    function ()
                    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55321328%2fsplitting-disjunctions-in-coq-hypothesis%23new-answer', 'question_page');

                    );

                    Post as a guest















                    Required, but never shown





















































                    Required, but never shown














                    Required, but never shown












                    Required, but never shown







                    Required, but never shown

































                    Required, but never shown














                    Required, but never shown












                    Required, but never shown







                    Required, but never shown







                    -

                    Popular posts from this blog

                    Kamusi Yaliyomo Aina za kamusi | Muundo wa kamusi | Faida za kamusi | Dhima ya picha katika kamusi | Marejeo | Tazama pia | Viungo vya nje | UrambazajiKuhusu kamusiGo-SwahiliWiki-KamusiKamusi ya Kiswahili na Kiingerezakuihariri na kuongeza habari

                    Image
                    Pages using ISBN magic linksMbegu za lughaKamusiIsimu nenoKiarabukitabulughaKiswahilialfabetimaanaufafanuzimanenomuhtasarisarufividahizoalfabeti Kamusi Kutoka Wikipedia, kamusi elezo huru Jump to navigation Jump to search Kamusi za Kiswahili Kamusi ya Kiswahili-Kiswahili (kamusi wahidiya) Kamusi ya Kiswahili - Kiingereza (kamusi thania) Kamusi (kutoka neno la Kiarabu قاموس qamus ) ni kitabu ambacho kinaorodhesha maneno ya lugha yaliyokusanywa kutoka kwa watumiaji wa lugha fulani, kwa mfano lugha ya Kiswahili. Maneno hupangwa kwa mtindo wa alfabeti, hutoa maana, asili na ufafanuzi wa utumizi wa maneno na jinsi yanavyotumika au yanavyotamkwa. [1] Yaliyomo 1 Aina za kamusi 2 Muundo wa kamusi 2.1 1. Utangulizi wa kamusi 2.2 2. Matini ya kamusi 2.3 3. Sherehe ya kamusi 3 Faida za kamusi 4 Dhima ya picha katika kamusi 5 Marejeo 6 Tazama pia 7 Viungo vya nje Aina za kamusi | Kuna aina mbalimbali za kamusi ambazo ni: Kamusi wahidiya yaani ya l
                    Read more

                    Swift 4 - func physicsWorld not invoked on collision? The Next CEO of Stack OverflowHow to call Objective-C code from Swift#ifdef replacement in the Swift language@selector() in Swift?#pragma mark in Swift?Swift for loop: for index, element in array?dispatch_after - GCD in Swift?Swift Beta performance: sorting arraysSplit a String into an array in Swift?The use of Swift 3 @objc inference in Swift 4 mode is deprecated?How to optimize UITableViewCell, because my UITableView lags

                    Image
                    Strange use of "whether ... than ..." in official text Could a dragon use its wings to swim? Car headlights in a world without electricity How to avoid supervisors with prejudiced views? Is the offspring between a demon and a celestial possible? If so what is it called and is it in a book somewhere? Can I board the first leg of the flight without having final country's PR card? subequations: How to continue numbering within subequation? How do you define an element with an ID attribute using LWC? Relevant Part for a Badminton Serve What CSS properties can the br tag have? What are the unusually-enlarged wing sections on this P-38 Lightning? Why did early computer designers eschew integers? Is it a bad idea to plug the other end of ESD strap to wall ground? Magento 1.9 observer on only new product added ( no updated product ) Airplane gently rocking its wings during whole flight It is correct to match light sources with the same color temperat
                    Read more

                    Access current req object everywhere in Node.js ExpressWhy are global variables considered bad practice? (node.js)Using req & res across functionsHow do I get the path to the current script with Node.js?What is Node.js' Connect, Express and “middleware”?Node.js w/ express error handling in callbackHow to access the GET parameters after “?” in Express?Modify Node.js req object parametersAccess “app” variable inside of ExpressJS/ConnectJS middleware?Node.js Express app - request objectAngular Http Module considered middleware?Session variables in ExpressJSAdd properties to the req object in expressjs with Typescript

                    Image
                    What steps should I take to lawfully visit the United States as a tourist immediately after visiting on a B-1 visa? Would dual wielding daggers be a viable choice for a covert bodyguard? For a hashing function like MD5, how similar can two plaintext strings be and still generate the same hash? Using Newton's shell theorem to accelerate a spaceship Why doesn't sea level show seasonality? What prevents someone from claiming to be the murderer in order to get the real murderer off? Has anyone in space seen or photographed a simple laser pointer from Earth? What does (void *)1 mean Why does the U.S. tolerate foreign influence from Saudi Arabia and Israel on its domestic policies while not tolerating that from China or Russia? Modulus Operandi What's the point of having a RAID 1 configuration over incremental backups to a secondary drive? How to ask for a LinkedIn endorsement? Good resources for solving techniques (Metaheuristics, MILP, CP etc) How woul
                    Read more